Embedded geometry: second order

This is the complete construction, rather than a proof of another claim.

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.

def finitePowerSeries (support : Finset ℕ) (a : ℕ → ℝ) (u : ℝ) : ℝ :=
  ∑ j ∈ support, a j * u ^ j

Exact module and namespace context

The later theorem identifies this expression with Mathlib's actual iterated derivative.

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.

def finitePowerSeriesDerivative
    (order : ℕ) (support : Finset ℕ) (a : ℕ → ℝ) (u : ℝ) : ℝ :=
  ∑ j ∈ support,
    (j.descFactorial order : ℝ) * a j * u ^ (j - order)

Exact module and namespace context

It is designed to pair with the hypothesis |u|≤1.

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.

def finitePowerSeriesDerivativeMass
    (order : ℕ) (support : Finset ℕ) (a : ℕ → ℝ) : ℝ :=
  ∑ j ∈ support, (j.descFactorial order : ℝ) * |a j|

Exact module and namespace context

The proof uses only standard smoothness rules.

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.

theorem finitePowerSeries_contDiff
    (support : Finset ℕ) (a : ℕ → ℝ) :
    ContDiff ℝ ⊤ (finitePowerSeries support a) := by
  unfold finitePowerSeries
  fun_prop

Exact module and namespace context

The proof reuses Mathlib's finite-sum and power derivative APIs.

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.

theorem iteratedDeriv_finitePowerSeries
    (order : ℕ) (support : Finset ℕ) (a : ℕ → ℝ) (u : ℝ) :
    iteratedDeriv order (finitePowerSeries support a) u =
      finitePowerSeriesDerivative order support a u := by
  unfold finitePowerSeries finitePowerSeriesDerivative
  rw [iteratedDeriv_fun_sum]
  · apply Finset.sum_congr rfl
    intro j hj
    simp [iteratedDeriv_pow]
    ring
  · intro j hj
    fun_prop

Exact module and namespace context

The proof combines the exact derivative identity with elementary absolute-value estimates.

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.

theorem abs_iteratedDeriv_finitePowerSeries_le_mass
    (order : ℕ) (support : Finset ℕ) (a : ℕ → ℝ) {u : ℝ}
    (hu : |u| ≤ 1) :
    |iteratedDeriv order (finitePowerSeries support a) u| ≤
      finitePowerSeriesDerivativeMass order support a := by
  rw [iteratedDeriv_finitePowerSeries]
  unfold finitePowerSeriesDerivative finitePowerSeriesDerivativeMass
  calc
    |∑ j ∈ support,
        (j.descFactorial order : ℝ) * a j * u ^ (j - order)| ≤
        ∑ j ∈ support,
          |(j.descFactorial order : ℝ) * a j * u ^ (j - order)| :=
      Finset.abs_sum_le_sum_abs _ _
    _ = ∑ j ∈ support,
        (j.descFactorial order : ℝ) * |a j| * |u| ^ (j - order) := by
      apply Finset.sum_congr rfl
      intro j hj
      rw [abs_mul, abs_mul, abs_pow,
        abs_of_nonneg (show 0 ≤ (j.descFactorial order : ℝ) by positivity)]
    _ ≤ ∑ j ∈ support, (j.descFactorial order : ℝ) * |a j| := by
      apply Finset.sum_le_sum
      intro j hj
      exact mul_le_of_le_one_right
        (mul_nonneg (by positivity) (abs_nonneg (a j)))
        (pow_le_one₀ (abs_nonneg u) hu)

Exact module and namespace context

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.

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