AutoSamplingTheory.TechnicalLemmas.Taylor

- A source-backed Hessian representative supplies the operator-norm bound on `fderiv (fderiv f)`. This is the reusable version of a SALD Brownian/Ito bridge: once source correspondence gives a Hessian field and a uniform bound for it, downstream proofs should consume this lemma rather than re-assuming the final operator bound.

theorem hessianOpNormOfSourceHessianField
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (f : E → ℝ)
    (sourceHessian : E → E →L[ℝ] (E →L[ℝ] ℝ))
    (C : ℝ)
    (hSourceHasHessian :
      ∀ z : E, HasFDerivAt (fderiv ℝ f) (sourceHessian z) z)
    (hSourceHessianBound :
      ∀ z : E, ‖sourceHessian z‖ ≤ C) :
    ∀ z : E, ‖fderiv ℝ (fderiv ℝ f) z‖ ≤ C := by
  intro z
  rw [(hSourceHasHessian z).fderiv]
  exact hSourceHessianBound z

/-- Convert an operator-norm bound on `fderiv (fderiv f)` to the corresponding
Mathlib `iteratedFDeriv` bound of order two. -/

AutoSamplingTheory/TechnicalLemmas/Taylor.lean:35published source at 77184245109a

- Convert an operator-norm bound on `fderiv (fderiv f)` to the corresponding Mathlib `iteratedFDeriv` bound of order two.

theorem iteratedFDerivTwoOpNormOfFDerivFDerivOpNorm
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (f : E → ℝ) (C : ℝ)
    (hHessianOpNorm :
      ∀ z : E, ‖fderiv ℝ (fderiv ℝ f) z‖ ≤ C) :
    ∀ z : E, ‖iteratedFDeriv ℝ 2 f z‖ ≤ C := by
  intro z
  have hnorm :
      ‖iteratedFDeriv ℝ 2 f z‖ =
        ‖fderiv ℝ (fderiv ℝ f) z‖ := by
    rw [← one_add_one_eq_two]
    rw [← norm_iteratedFDeriv_fderiv (𝕜 := ℝ) (f := f) (x := z) (n := 1)]
    rw [norm_iteratedFDeriv_one]
  rw [hnorm]
  exact hHessianOpNorm z

/-- Standard orthonormal-basis vectors are unit directions. -/

AutoSamplingTheory/TechnicalLemmas/Taylor.lean:51published source at 77184245109a

- Standard orthonormal-basis vectors are unit directions.

theorem stdOrthonormalBasisUnit
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] (i : Fin (Module.finrank ℝ E)) :
    ‖(stdOrthonormalBasis ℝ E) i‖ ≤ (1 : ℝ) := by
  rw [OrthonormalBasis.norm_eq_one]

/-- Algebraic packaging for quadratic-variation normalization. -/

AutoSamplingTheory/TechnicalLemmas/Taylor.lean:68published source at 77184245109a

- Algebraic packaging for quadratic-variation normalization.

theorem quadraticVariationNormalizationOfCoeffDefAndVarianceOne
    {α : Type*}
    (quadraticCoeff variance generator : α → ℝ)
    (hQuadraticCoeffDef : ∀ a, quadraticCoeff a = generator a)
    (hVarianceOne : ∀ a, variance a = 1) :
    ∀ a, quadraticCoeff a * variance a = generator a := by
  intro a
  rw [hQuadraticCoeffDef a, hVarianceOne a, mul_one]

end Taylor
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Taylor.lean:75published source at 77184245109a