OAI/Geometry/RCD/Coordinates/RegularSelectedMass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RegularPointCoordinates.RegularPatchSelection.operator line 26
2. def OAI.RegularPointCoordinates.RegularPatchSelection.activePatchesAt line 29
3. theorem OAI.RegularPointCoordinates.RegularPatchSelection.cumulative line 35

   Source documentation

   Both cumulative estimates now concern the actual active net and its fixed energy centers, including the original singular Bochner mass.

   theorem cumulative (hzeta : 0 ≤ zeta) (hzeta1 : zeta ≤ 1 / 64)
       (hCχ : 0 ≤ Cχ) (henlargement : 1 ≤ enlargement)
       (hsmall : (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * ((1 / 8 : ℝ) ^ n)⁻¹) * zeta) ≤ 1 / 2)
       (hnear : (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * ((1 / 2 : ℝ) ^ n)⁻¹) * zeta) ≤ 1 / 4) :
       ∃ Theta tau : ℝ, 0 < Theta ∧ 0 < tau ∧ ∀ epsilon : ℝ, 0 ≤ epsilon → epsilon ≤ tau →
       (∀ i, 4 * pinchingMassUnitFactor n * regularSmallMassCoefficient n Cχ *
         (zeta + |K| * (e.heat.radius / (2 : ℝ) ^ (e.heat.shift + i + 15)) ^ 2) ≤ epsilon) →
       ∀ q, q ∈ e.heat.patchRegion → ∀ (xi : Euclidean n) (k : ℕ),
         (‖xi‖ ^ 2 + ∑ i ∈ Finset.range k, ⟪xi, patchMass (p.activePatchesAt q i) (p.operator i) xi⟫_ℝ ≤
           Theta * ‖e.heat.frozenAt q k xi‖ ^ 2) ∧
         (‖e.heat.frozenAt q k xi‖ ^ 2 ≤ Theta * (‖xi‖ ^ 2 + ∑ i ∈ Finset.range k,
           ⟪xi, patchPrincipal (p.activePatchesAt q i) (fun y => e.heat.patchCutoff psi.value i y (e.heat.values q))
   …

   Mentions: OAI.RegularPointCoordinates.tau, OAI.RegularPointCoordinates.pinchingMassUnitFactor, OAI.RegularPointCoordinates.regularSmallMassCoefficient, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.patchMass, OAI.RegularPointCoordinates.patchPrincipal

4. theorem OAI.RegularPointCoordinates.RegularPatchSelection.mass_small line 77

   Source documentation

   At one scale the total positive mass costs only the active overlap, with the coefficient computed from the original Bochner cutoff bound.

   theorem mass_small (hzeta : 0 ≤ zeta) (hzeta1 : zeta ≤ 1 / 64) (hCχ : 0 ≤ Cχ)
       (hsmall : (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * ((1 / 8 : ℝ) ^ n)⁻¹) * zeta) ≤ 1 / 2)
       (hnear : (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * ((1 / 64 : ℝ) ^ n)⁻¹) * zeta) ≤ 1 / 4)
       (i : ℕ) {epsilon : ℝ}
       (hcoef : (patchOverlapBound n (1 / 2) 2 3 : ℝ) *
         (4 * pinchingMassUnitFactor n * regularSmallMassCoefficient n Cχ *
           (zeta + |K| * (e.heat.radius / 2 ^ (e.heat.shift + i + 15)) ^ 2)) ≤ epsilon)
       {q : X} (hq : q ∈ e.heat.patchRegion) (xi : Euclidean n) :
       ⟪xi, patchMass (p.activePatchesAt q i) (p.operator i) xi⟫_ℝ ≤
         epsilon * ‖e.heat.frozenAt q i xi‖ ^ 2 := by
   …

   Mentions: OAI.RegularPointCoordinates.patchOverlapBound, OAI.RegularPointCoordinates.pinchingMassUnitFactor, OAI.RegularPointCoordinates.regularSmallMassCoefficient, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.patchMass