FullMassPinching.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Directional pinching from the actual full residual mass

theorem OAI.RegularPointCoordinates.directional_mass_from_cutoff_residual line 24

Source documentation

The full measure of the actual coordinate displacement is controlled by the Poisson-difference mass, the residual gradient and the constant-direction error. The residual mass is derived from its Bochner equation and the cutoff.

theorem directional_mass_from_cutoff_residual
    (U : F →L[ℝ] SobolevSpace μ hQ) (A : E →L[ℝ] F)
    (M : PositiveBilinearMeasure X F) (a : F) (b δ : E)
    {p : X} {r ρ C κ β d P K : ℝ} {L : ℝ≥0}
    (χ : GoodLaplacianCutoff μ hQ p ρ C) (hρ : 0 < ρ) (hρr : ρ < r)
    (hC : 0 ≤ C) (hκ : 0 ≤ κ) (hK : 0 ≤ K)
    (hvol : 0 < μ.real (ball p ρ))
    (hnormal : sobolevMeanGram μ hQ (U.comp A) (ball p ρ) measurableSet_ball =
      ContinuousLinearMap.id ℝ E)
    (G : LocalHarmonicEnergy μ hQ U M κ p r L (a - A b))
    (hgradient : ∀ᵐ x ∂μ.restrict (closedBall p (2 * ρ)),
      localGamma μ hQ (U (a - A b)) (U (a - A b)) x ≤ β)
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.sobolevMeanGram, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.localGamma

theorem OAI.RegularPointCoordinates.directional_mass_from_gradient_bounds line 102

Source documentation

A coordinate gradient bound also supplies the full mass upper bound used in coefficient transfer, through the same local Bochner family. No separate trace or coordinate mass estimate is assumed.

theorem directional_mass_from_gradient_bounds
    (U : F →L[ℝ] SobolevSpace μ hQ) (A : E →L[ℝ] F)
    (M : PositiveBilinearMeasure X F) (a : F) (b δ : E)
    {p : X} {r ρ C κ β d P H : ℝ} {L : ℝ≥0}
    (χ : GoodLaplacianCutoff μ hQ p ρ C) (hρ : 0 < ρ) (hρr : ρ < r)
    (hC : 0 ≤ C) (hκ : 0 ≤ κ) (hH : 0 ≤ H)
    (hvol : 0 < μ.real (ball p ρ))
    (hnormal : sobolevMeanGram μ hQ (U.comp A) (ball p ρ) measurableSet_ball =
      ContinuousLinearMap.id ℝ E)
    (G : ∀ v, LocalHarmonicEnergy μ hQ U M κ p r L v)
    (hgradient : ∀ᵐ x ∂μ.restrict (closedBall p (2 * ρ)),
      localGamma μ hQ (U (a - A b)) (U (a - A b)) x ≤ β)
…

theorem OAI.RegularPointCoordinates.directional_mass_from_pairing_bounds line 140

Source documentation

Constant-direction pairings give the displacement estimate needed in full-mass pinching. Thus the averaged-gradient comparison is a conclusion, not an extra hypothesis of the mass estimate.

theorem directional_mass_from_pairing_bounds
    (U : F →L[ℝ] SobolevSpace μ hQ) (A : E →L[ℝ] F)
    (Hpair : E →L[ℝ] SobolevSpace μ hQ)
    (M : PositiveBilinearMeasure X F) (a : F) (b δ : E)
    {p : X} {r ρ C κ β P H D : ℝ} {L : ℝ≥0}
    (χ : GoodLaplacianCutoff μ hQ p ρ C) (hρ : 0 < ρ) (hρr : ρ < r)
    (hC : 0 ≤ C) (hκ : 0 ≤ κ) (hH : 0 ≤ H) (hD : 0 ≤ D)
    (hvol : 0 < μ.real (ball p ρ))
    (hfin : μ (ball p ρ) ≠ ∞) (hpos : μ (ball p ρ) ≠ 0)
    (hnormal : sobolevMeanGram μ hQ (U.comp A) (ball p ρ) measurableSet_ball =
      ContinuousLinearMap.id ℝ E)
    (G : ∀ v, LocalHarmonicEnergy μ hQ U M κ p r L v)
…