PatchSecondDerivative.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The second directional derivative of the patch field

This proves the actual derivative formula and the frozen dual-norm bound in re:field-second. The only nonzero terms differentiate the cutoff twice, or differentiate the cutoff and the affine factor once each.

theorem OAI.RegularPointCoordinates.cutoff_affine_second_directional line 27

Source documentation

The second directional derivative of a cutoff times an affine map.

theorem cutoff_affine_second_directional (phi : E → ℝ) (D : E →L[ℝ] F)
    (c P xi : E) (hphi : ContDiffAt ℝ 2 phi P) :
    fderiv ℝ (fun y => fderiv ℝ (fun z => phi z • D (z - c)) y xi) P xi =
      fderiv ℝ (fun y => fderiv ℝ phi y xi) P xi • D (P - c) +
        (2 * fderiv ℝ phi P xi) • D xi := by
…

theorem OAI.RegularPointCoordinates.second_directional_finset_sum line 60

Source documentation

Finite sums commute with the actual second directional derivative.

theorem second_directional_finset_sum (s : Finset ι) (f : ι → E → F) (P xi : E)
    (hf : ∀ j ∈ s, ContDiffAt ℝ 2 (f j) P) :
    fderiv ℝ (fun y => fderiv ℝ (fun z => ∑ j ∈ s, f j z) y xi) P xi =
      ∑ j ∈ s, fderiv ℝ (fun y => fderiv ℝ (f j) y xi) P xi := by
…

theorem OAI.RegularPointCoordinates.patchField_second_directional line 86

Source documentation

The full finite-patch formula from local twice continuous differentiability of the cutoff functions.

theorem patchField_second_directional (s : Finset ι) (phi : ι → E → ℝ)
    (D : ι → E →L[ℝ] E) (c : ι → E) (P xi : E)
    (hphi : ∀ j ∈ s, ContDiffAt ℝ 2 (phi j) P) :
    fderiv ℝ (fun y => fderiv ℝ (patchField s phi D c) y xi) P xi =
      ∑ j ∈ s, (fderiv ℝ (fun y => fderiv ℝ (phi j) y xi) P xi • D j (P - c j) +
        (2 * fderiv ℝ (phi j) P xi) • D j xi) := by
…

Mentions: OAI.RegularPointCoordinates.patchField

theorem OAI.RegularPointCoordinates.frozen_patch_directional_sum_le line 106

Source documentation

A derivative-weighted sum of mass values retains the square root of the total directional mass.

theorem frozen_patch_directional_sum_le (T : E ≃L[ℝ] E) (s : Finset ι)
    (D : ι → E →L[ℝ] E) (a : ι → ℝ) (xi : E) {N : ℕ} {epsilon A : ℝ}
    (hN : s.card ≤ N) (hepsilon : 0 ≤ epsilon) (hA : 0 ≤ A)
    (hD : ∀ j ∈ s, (D j).IsPositive)
    (hZ : ∀ x, ⟪x, patchMass s D x⟫_ℝ ≤ epsilon * ‖T x‖ ^ 2)
    (ha : ∀ j ∈ s, |a j| ≤ A) :
    ‖(T.symm : E →L[ℝ] E).adjoint (patchCutoffError s D (fun _ => xi) a)‖ ≤
      A * Real.sqrt epsilon * Real.sqrt (N : ℝ) *
        Real.sqrt ⟪xi, patchMass s D xi⟫_ℝ := by
…

Mentions: OAI.RegularPointCoordinates.patchMass, OAI.RegularPointCoordinates.patchCutoffError

theorem OAI.RegularPointCoordinates.patchField_second_directional_frozen_le_sqrt line 141

Source documentation

The second derivative estimate with the small factor retained.

theorem patchField_second_directional_frozen_le_sqrt (T : E ≃L[ℝ] E) (s : Finset ι)
    (phi : ι → E → ℝ) (D : ι → E →L[ℝ] E) (c : ι → E) (P xi : E) {N : ℕ}
    {epsilon C K r energy : ℝ} (hN : s.card ≤ N)
    (hepsilon : 0 ≤ epsilon) (hC : 0 ≤ C) (hK : 0 ≤ K)
    (hr : 0 < r) (henergy : 0 ≤ energy)
    (hphi : ∀ j ∈ s, ContDiffAt ℝ 2 (phi j) P)
    (hD : ∀ j ∈ s, (D j).IsPositive)
    (hZ : ∀ x, ⟪x, patchMass s D x⟫_ℝ ≤ epsilon * ‖T x‖ ^ 2)
    (hw : ∀ j ∈ s, ⟪P - c j, D j (P - c j)⟫_ℝ ≤ C * r ^ 2 * energy)
    (hfirst : ∀ j ∈ s, |fderiv ℝ (phi j) P xi| ≤ K / r * ‖T xi‖)
    (hsecond : ∀ j ∈ s, |fderiv ℝ (fun y => fderiv ℝ (phi j) y xi) P xi| ≤
      K / r ^ 2 * ‖T xi‖ ^ 2) :
…

Mentions: OAI.RegularPointCoordinates.patchMass

theorem OAI.RegularPointCoordinates.patchField_second_directional_frozen_le line 190

Source documentation

With epsilon ≤ 1, the small factor may be dropped, giving the two terms in re:field-second with explicit overlap and cutoff constants.

theorem patchField_second_directional_frozen_le (T : E ≃L[ℝ] E) (s : Finset ι)
    (phi : ι → E → ℝ) (D : ι → E →L[ℝ] E) (c : ι → E) (P xi : E) {N : ℕ}
    {epsilon C K r energy : ℝ} (hN : s.card ≤ N)
    (hepsilon : 0 ≤ epsilon) (hepsilon1 : epsilon ≤ 1) (hC : 0 ≤ C) (hK : 0 ≤ K)
    (hr : 0 < r) (henergy : 0 ≤ energy)
    (hphi : ∀ j ∈ s, ContDiffAt ℝ 2 (phi j) P)
    (hD : ∀ j ∈ s, (D j).IsPositive)
    (hZ : ∀ x, ⟪x, patchMass s D x⟫_ℝ ≤ epsilon * ‖T x‖ ^ 2)
    (hw : ∀ j ∈ s, ⟪P - c j, D j (P - c j)⟫_ℝ ≤ C * r ^ 2 * energy)
    (hfirst : ∀ j ∈ s, |fderiv ℝ (phi j) P xi| ≤ K / r * ‖T xi‖)
    (hsecond : ∀ j ∈ s, |fderiv ℝ (fun y => fderiv ℝ (phi j) y xi) P xi| ≤
      K / r ^ 2 * ‖T xi‖ ^ 2) :
…

Mentions: OAI.RegularPointCoordinates.patchMass