OAI/Geometry/RCD/Coordinates/PatchDirectionalBounds.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Directional estimates for finite patch fields

The finite set is the set of active patches at the point under consideration. All metric norms are frozen using a continuous linear equivalence T. The hypotheses are the individual displacement energies, cutoff derivative bounds, overlap bound, and positive mass bounds; no field estimate is assumed.

  1. def OAI.RegularPointCoordinates.patchMass line 24

    Source documentation

    The unweighted mass of the active patches.

    def patchMass (s : Finset ι) (D : ι → E →L[ℝ] E) : E →L[ℝ] E :=
…
  2. def OAI.RegularPointCoordinates.patchPrincipal line 28

    Source documentation

    The principal part of the derivative of the patch field.

    def patchPrincipal (s : Finset ι) (phi : ι → ℝ) (D : ι → E →L[ℝ] E) :
    E →L[ℝ] E := ∑ j ∈ s, phi j • D j
  3. def OAI.RegularPointCoordinates.patchCutoffError line 32

    Source documentation

    The error produced by differentiating the cutoff functions.

    def patchCutoffError (s : Finset ι) (D : ι → E →L[ℝ] E)
    (w : ι → E) (a : ι → ℝ) : E := ∑ j ∈ s, a j • D j (w j)
  4. theorem OAI.RegularPointCoordinates.patchMass_isPositive line 35
  5. theorem OAI.RegularPointCoordinates.inner_patchMass line 39
  6. theorem OAI.RegularPointCoordinates.patch_form_le_mass line 44

    Source documentation

    Each positive patch is bounded above by the total positive mass.

    theorem patch_form_le_mass (s : Finset ι) (D : ι → E →L[ℝ] E)
    (hD : ∀ j ∈ s, (D j).IsPositive) {j : ι} (hj : j ∈ s) (x : E) :
    ⟪x, D j x⟫_ℝ ≤ ⟪x, patchMass s D x⟫_ℝ := by
…

    Mentions: OAI.RegularPointCoordinates.patchMass

  7. theorem OAI.RegularPointCoordinates.patchPrincipal_form_le_mass line 51

    Source documentation

    Nonnegative cutoffs bounded by one give 0 ≤ S ≤ Z.

    theorem patchPrincipal_form_le_mass (s : Finset ι) (phi : ι → ℝ)
    (D : ι → E →L[ℝ] E) (hD : ∀ j ∈ s, (D j).IsPositive)
    (hphi : ∀ j ∈ s, phi j ≤ 1) (x : E) :
    ⟪x, patchPrincipal s phi D x⟫_ℝ ≤ ⟪x, patchMass s D x⟫_ℝ := by
…

    Mentions: OAI.RegularPointCoordinates.patchPrincipal, OAI.RegularPointCoordinates.patchMass

  8. theorem OAI.RegularPointCoordinates.patchPrincipal_frozen_norm_le line 66

    Source documentation

    The cumulative smallness Z ≤ epsilon H gives the sharp principal bound. Individual smallness of each patch alone is not used as a substitute for this cumulative hypothesis.

    theorem patchPrincipal_frozen_norm_le (T : E ≃L[ℝ] E) (s : Finset ι)
    (phi : ι → ℝ) (D : ι → E →L[ℝ] E) {epsilon : ℝ}
    (hepsilon : 0 ≤ epsilon) (hD : ∀ j ∈ s, (D j).IsPositive)
    (hphi0 : ∀ j ∈ s, 0 ≤ phi j) (hphi1 : ∀ j ∈ s, phi j ≤ 1)
    (hZ : ∀ x, ⟪x, patchMass s D x⟫_ℝ ≤ epsilon * ‖T x‖ ^ 2) (xi : E) :
    ‖(T.symm : E →L[ℝ] E).adjoint (patchPrincipal s phi D xi)‖ ≤
      Real.sqrt epsilon * Real.sqrt ⟪xi, patchMass s D xi⟫_ℝ := by
…

    Mentions: OAI.RegularPointCoordinates.patchMass, OAI.RegularPointCoordinates.patchPrincipal

  9. theorem OAI.RegularPointCoordinates.frozen_patch_weighted_value_le line 80

    Source documentation

    A weighted finite patch sum in the dual metric.

    theorem frozen_patch_weighted_value_le (T : E ≃L[ℝ] E) (s : Finset ι)
    (D : ι → E →L[ℝ] E) (w : ι → E) (a : ι → ℝ) {N : ℕ}
    {epsilon C r energy A : ℝ} (hN : s.card ≤ N)
    (hepsilon : 0 ≤ epsilon) (hC : 0 ≤ C) (hr : 0 ≤ r)
    (henergy : 0 ≤ energy) (hA : 0 ≤ A)
    (hD : ∀ j ∈ s, (D j).IsPositive)
    (hsmall : ∀ j ∈ s, ∀ x, ⟪x, D j x⟫_ℝ ≤ epsilon * ‖T x‖ ^ 2)
    (hw : ∀ j ∈ s, ⟪w j, D j (w j)⟫_ℝ ≤ C * r ^ 2 * energy)
    (ha : ∀ j ∈ s, |a j| ≤ A) :
    ‖(T.symm : E →L[ℝ] E).adjoint (patchCutoffError s D w a)‖ ≤
      (N : ℝ) * A * (Real.sqrt epsilon * Real.sqrt C * r * Real.sqrt energy) := by
…

    Mentions: OAI.RegularPointCoordinates.patchCutoffError

  10. theorem OAI.RegularPointCoordinates.patchField_frozen_value_le line 109

    Source documentation

    The normalized value estimate re:field-value.

    theorem patchField_frozen_value_le (T : E ≃L[ℝ] E) (s : Finset ι)
    (phi : ι → E → ℝ) (D : ι → E →L[ℝ] E) (c : ι → E) (P : E) {N : ℕ}
    {epsilon C r energy : ℝ} (hN : s.card ≤ N)
    (hepsilon : 0 ≤ epsilon) (hC : 0 ≤ C) (hr : 0 < r) (henergy : 0 ≤ energy)
    (hD : ∀ j ∈ s, (D j).IsPositive)
    (hsmall : ∀ j ∈ s, ∀ x, ⟪x, D j x⟫_ℝ ≤ epsilon * ‖T x‖ ^ 2)
    (hw : ∀ j ∈ s, ⟪P - c j, D j (P - c j)⟫_ℝ ≤ C * r ^ 2 * energy)
    (hphi : ∀ j ∈ s, |phi j P| ≤ 1) :
    ‖(T.symm : E →L[ℝ] E).adjoint (patchField s phi D c P)‖ / r ≤
      (N : ℝ) * Real.sqrt C * Real.sqrt epsilon * Real.sqrt energy := by
…

    Mentions: OAI.RegularPointCoordinates.patchField

  11. theorem OAI.RegularPointCoordinates.patchCutoffError_frozen_norm_le line 127

    Source documentation

    The dual norm estimate for the linear cutoff error.

    theorem patchCutoffError_frozen_norm_le (T : E ≃L[ℝ] E) (s : Finset ι)
    (D : ι → E →L[ℝ] E) (w : ι → E) (a : ι → ℝ) (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)
    (hD : ∀ j ∈ s, (D j).IsPositive)
    (hsmall : ∀ j ∈ s, ∀ x, ⟪x, D j x⟫_ℝ ≤ epsilon * ‖T x‖ ^ 2)
    (hw : ∀ j ∈ s, ⟪w j, D j (w j)⟫_ℝ ≤ C * r ^ 2 * energy)
    (ha : ∀ j ∈ s, |a j| ≤ K / r * ‖T xi‖) :
    ‖(T.symm : E →L[ℝ] E).adjoint (patchCutoffError s D w a)‖ ≤
      (N : ℝ) * K * Real.sqrt C * Real.sqrt epsilon * Real.sqrt energy * ‖T xi‖ := by
…

    Mentions: OAI.RegularPointCoordinates.patchCutoffError

  12. theorem OAI.RegularPointCoordinates.sqrt_patch_energy_sum_le line 145

    Source documentation

    Bounded overlap controls the total displacement energy.

    theorem sqrt_patch_energy_sum_le (s : Finset ι) (D : ι → E →L[ℝ] E)
    (w : ι → E) {N : ℕ} {C r energy : ℝ} (hN : s.card ≤ N)
    (hC : 0 ≤ C) (hr : 0 ≤ r) (henergy : 0 ≤ energy)
    (hD : ∀ j ∈ s, (D j).IsPositive)
    (hw : ∀ j ∈ s, ⟪w j, D j (w j)⟫_ℝ ≤ C * r ^ 2 * energy) :
    Real.sqrt (∑ j ∈ s, ⟪w j, D j (w j)⟫_ℝ) ≤
      Real.sqrt ((N : ℝ) * C) * r * Real.sqrt energy := by
…
  13. theorem OAI.RegularPointCoordinates.patchCutoffError_diagonal_le line 171

    Source documentation

    The sharp diagonal estimate retains the directional mass Z[xi]. It does not replace this mass by a bound in terms of the whole source metric.

    theorem patchCutoffError_diagonal_le (T : E ≃L[ℝ] E) (s : Finset ι)
    (D : ι → E →L[ℝ] E) (w : ι → E) (a : ι → ℝ) (xi : E) {N : ℕ}
    {C K r energy : ℝ} (hN : s.card ≤ N) (hC : 0 ≤ C) (hK : 0 ≤ K)
    (hr : 0 < r) (henergy : 0 ≤ energy)
    (hD : ∀ j ∈ s, (D j).IsPositive)
    (hw : ∀ j ∈ s, ⟪w j, D j (w j)⟫_ℝ ≤ C * r ^ 2 * energy)
    (ha : ∀ j ∈ s, |a j| ≤ K / r * ‖T xi‖) :
    |⟪xi, patchCutoffError s D w a⟫_ℝ| ≤
      K * Real.sqrt ((N : ℝ) * C) *
        Real.sqrt ⟪xi, patchMass s D xi⟫_ℝ * Real.sqrt energy * ‖T xi‖ := by
…

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

  14. theorem OAI.RegularPointCoordinates.fderiv_patchField_apply line 194

    Source documentation

    The bounds above apply to the actual derivative, with the exact principal and cutoff-error decomposition supplied by differentiation.

    theorem fderiv_patchField_apply (s : Finset ι) (phi : ι → E → ℝ)
    (dphi : ι → E →L[ℝ] ℝ) (D : ι → E →L[ℝ] E) (c : ι → E) (P xi : E)
    (hphi : ∀ j ∈ s, HasFDerivAt (phi j) (dphi j) P) :
    fderiv ℝ (patchField s phi D c) P xi =
      patchPrincipal s (fun j => phi j P) D xi +
        patchCutoffError s D (fun j => P - c j) (fun j => dphi j xi) := by
…

    Mentions: OAI.RegularPointCoordinates.patchField, OAI.RegularPointCoordinates.patchPrincipal, OAI.RegularPointCoordinates.patchCutoffError