Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

A fourth-order composition budget

AutoSamplingTheory.TechnicalLemmas.Analysis.FinitePowerSeries.fourthOrderCompositionExpression_abs_le · theorem · Teaching coverage

Read this first

Mathematical statement

Bounds on the first four outer derivatives control the exact five-term scalar fourth-order chain-rule expression.

\[|k_4u_1^4+6k_3u_1^2u_2+3k_2u_2^2+4k_2u_1u_3+k_1u_4|\le A_4|u_1|^4+6A_3|u_1|^2|u_2|+3A_2|u_2|^2+4A_2|u_1||u_3|+A_1|u_4|\]
Lean statement · fourthOrderCompositionExpression_abs_le

The numerical coefficients are explicit rather than hidden in a generic constant.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
theorem fourthOrderCompositionExpression_abs_le
    {k1 k2 k3 k4 u1 u2 u3 u4 A1 A2 A3 A4 : ℝ}
    (hk1 : |k1| ≤ A1) (hk2 : |k2| ≤ A2)
    (hk3 : |k3| ≤ A3) (hk4 : |k4| ≤ A4) :
    |k4 * u1 ^ (4 : ℕ) +
        6 * k3 * u1 ^ (2 : ℕ) * u2 +
        3 * k2 * u2 ^ (2 : ℕ) +
        4 * k2 * u1 * u3 + k1 * u4| ≤
      A4 * |u1| ^ (4 : ℕ) +
        6 * A3 * |u1| ^ (2 : ℕ) * |u2| +
        3 * A2 * |u2| ^ (2 : ℕ) +
        4 * A2 * |u1| * |u3| + A1 * |u4|

Exact module and namespace context

Proof roadmap

  1. 1Split the five terms

    The coefficients 1,6,3,4,1 are the exact one-dimensional fourth-order chain-rule coefficients.

  2. 2Bound each term

    Apply the triangle inequality and then substitute |k_i|≤A_i.

Full assumptions and notation

All objects and hypotheses

  • |k_i|≤A_i for i=1,2,3,4.
  • The inner derivative values are arbitrary reals.
  • No sign assumption is used.

Mathematical proof

1. Split the five terms

The coefficients 1,6,3,4,1 are the exact one-dimensional fourth-order chain-rule coefficients.

\[t_1=k_4u_1^4,\ldots,t_5=k_1u_4\]
Corresponding Lean step

The proof names the five summands.

2. Bound each term

Apply the triangle inequality and then substitute |k_i|≤A_i.

\[|\sum_i t_i|\le\sum_i|t_i|\le\text{displayed majorant}\]
Corresponding Lean step

abs_add_le, abs_mul, and monotone multiplication give the result.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · fourthOrderCompositionExpression_abs_le

This is a scalar inequality; Mathlib's chain rule can identify the derivative values separately.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
theorem fourthOrderCompositionExpression_abs_le
    {k1 k2 k3 k4 u1 u2 u3 u4 A1 A2 A3 A4 : ℝ}
    (hk1 : |k1| ≤ A1) (hk2 : |k2| ≤ A2)
    (hk3 : |k3| ≤ A3) (hk4 : |k4| ≤ A4) :
    |k4 * u1 ^ (4 : ℕ) +
        6 * k3 * u1 ^ (2 : ℕ) * u2 +
        3 * k2 * u2 ^ (2 : ℕ) +
        4 * k2 * u1 * u3 + k1 * u4| ≤
      A4 * |u1| ^ (4 : ℕ) +
        6 * A3 * |u1| ^ (2 : ℕ) * |u2| +
        3 * A2 * |u2| ^ (2 : ℕ) +
        4 * A2 * |u1| * |u3| + A1 * |u4| := by
  let t1 := k4 * u1 ^ (4 : ℕ)
  let t2 := 6 * k3 * u1 ^ (2 : ℕ) * u2
  let t3 := 3 * k2 * u2 ^ (2 : ℕ)
  let t4 := 4 * k2 * u1 * u3
  let t5 := k1 * u4
  have htri : |t1 + t2 + t3 + t4 + t5| ≤
      |t1| + |t2| + |t3| + |t4| + |t5| := by
    calc
      |t1 + t2 + t3 + t4 + t5| ≤ |t1 + t2 + t3 + t4| + |t5| :=
        abs_add_le _ _
      _ ≤ (|t1 + t2 + t3| + |t4|) + |t5| := by
        gcongr
        exact abs_add_le _ _
      _ ≤ ((|t1 + t2| + |t3|) + |t4|) + |t5| := by
        gcongr
        exact abs_add_le _ _
      _ ≤ (((|t1| + |t2|) + |t3|) + |t4|) + |t5| := by
        gcongr
        exact abs_add_le _ _
  have ht1 : |t1| ≤ A4 * |u1| ^ (4 : ℕ) := by
    dsimp [t1]
    rw [abs_mul, abs_pow]
    exact mul_le_mul_of_nonneg_right hk4 (by positivity)
  have ht2 : |t2| ≤ 6 * A3 * |u1| ^ (2 : ℕ) * |u2| := by
    dsimp [t2]
    rw [abs_mul, abs_mul, abs_mul, abs_pow]
    norm_num
    gcongr
  have ht3 : |t3| ≤ 3 * A2 * |u2| ^ (2 : ℕ) := by
    dsimp [t3]
    rw [abs_mul, abs_mul, abs_pow]
    norm_num
    gcongr
  have ht4 : |t4| ≤ 4 * A2 * |u1| * |u3| := by
    dsimp [t4]
    rw [abs_mul, abs_mul, abs_mul]
    norm_num
    gcongr
  have ht5 : |t5| ≤ A1 * |u4| := by
    dsimp [t5]
    rw [abs_mul]
    exact mul_le_mul_of_nonneg_right hk1 (abs_nonneg _)
  dsimp [t1, t2, t3, t4, t5] at htri
  linarith

end AutoSamplingTheory.TechnicalLemmas.Analysis.FinitePowerSeries

Exact module and namespace context

Scope and omitted-condition boundaries
  • It does not itself prove differentiability of a particular composition.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

    Mathlib API called (external library)

    No direct Mathlib call recorded; see the Samplinglib parents.

    Mathematical sources

    Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.