EuclideanAffineTaylor.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A quantitative affine Taylor bound in the actual local L² space

The only analytic hypothesis is an interior second derivative bound. The scale factor is exactly quadratic; no affine approximation hypothesis is used. This is the Euclidean calculation in harmonic affine improvement.

theorem OAI.RegularPointCoordinates.affine_taylor_bound_on_ball line 24

Source documentation

Taylor's estimate on every radial segment of an interior ball.

theorem affine_taylor_bound_on_ball {f : E → ℝ} {df : E → E →L[ℝ] ℝ}
    {ddf : E → E →L[ℝ] (E →L[ℝ] ℝ)} {r R C : ℝ}
    (hr : 0 < r) (hrR : r ≤ R) (hC : 0 ≤ C)
    (hf : ∀ z ∈ ball (0 : E) R, HasFDerivAt f (df z) z)
    (hdf : ∀ z ∈ ball (0 : E) R, HasFDerivAt df (ddf z) z)
    (hbound : ∀ z ∈ ball (0 : E) R, ‖ddf z‖ ≤ C)
    {z : E} (hz : z ∈ ball (0 : E) r) :
    |f z - f 0 - df 0 z| ≤ C * r ^ 2 := by
…

theorem OAI.RegularPointCoordinates.l2_affine_taylor_bound line 44

Source documentation

The radial Taylor polynomial bounds the local L² error. The norm of the constant function records the square root of the ball's measure.

theorem l2_affine_taylor_bound (μ : Measure E)
    {f : E → ℝ} {df : E → E →L[ℝ] ℝ}
    {ddf : E → E →L[ℝ] (E →L[ℝ] ℝ)} {r R C : ℝ}
    (hr : 0 < r) (hrR : r ≤ R) (hC : 0 ≤ C)
    (hf : ∀ z ∈ ball (0 : E) R, HasFDerivAt f (df z) z)
    (hdf : ∀ z ∈ ball (0 : E) R, HasFDerivAt df (ddf z) z)
    (hbound : ∀ z ∈ ball (0 : E) R, ‖ddf z‖ ≤ C)
    (F A one : Lp ℝ 2 (μ.restrict (ball (0 : E) r)))
    (hF : F =ᵐ[μ.restrict (ball (0 : E) r)] f)
    (hA : A =ᵐ[μ.restrict (ball (0 : E) r)] fun z => f 0 + df 0 z)
    (hone : one =ᵐ[μ.restrict (ball (0 : E) r)] fun _ => (1 : ℝ)) :
    ‖F - A‖ ≤ C * r ^ 2 * ‖one‖ := by
…

theorem OAI.RegularPointCoordinates.euclidean_linear_form_sum line 65
Source documentation
Evaluation of a linear form in the standard Euclidean coordinates.
```
theorem euclidean_linear_form_sum {n : ℕ} (ell : Euclidean n →L[ℝ] ℝ)
    (z : Euclidean n) :
    (∑ i, ell (EuclideanSpace.single i 1) * z i) = ell z := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.l2_coordinate_affine_taylor_bound line 79

Source documentation

The Taylor polynomial is an actual affine combination of the constant and coordinate functions in the local L² space.

theorem l2_coordinate_affine_taylor_bound {n : ℕ} (μ : Measure (Euclidean n))
    {f : Euclidean n → ℝ} {df : Euclidean n → Euclidean n →L[ℝ] ℝ}
    {ddf : Euclidean n → Euclidean n →L[ℝ] (Euclidean n →L[ℝ] ℝ)}
    {r R C : ℝ} (hr : 0 < r) (hrR : r ≤ R) (hC : 0 ≤ C)
    (hf : ∀ z ∈ ball (0 : Euclidean n) R, HasFDerivAt f (df z) z)
    (hdf : ∀ z ∈ ball (0 : Euclidean n) R, HasFDerivAt df (ddf z) z)
    (hbound : ∀ z ∈ ball (0 : Euclidean n) R, ‖ddf z‖ ≤ C)
    (F one : Lp ℝ 2 (μ.restrict (ball (0 : Euclidean n) r)))
    (u : Fin n → Lp ℝ 2 (μ.restrict (ball (0 : Euclidean n) r)))
    (hF : F =ᵐ[μ.restrict (ball (0 : Euclidean n) r)] f)
    (hone : one =ᵐ[μ.restrict (ball (0 : Euclidean n) r)] fun _ => (1 : ℝ))
    (hu : ∀ i, u i =ᵐ[μ.restrict (ball (0 : Euclidean n) r)] fun z => z i) :
…

Mentions: OAI.RegularPointCoordinates.Euclidean