NormalizedBochnerMass.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Scaled Bochner mass from a first-order splitting map

This connects the actual averaged component errors in the splitting hypothesis to the dimensionless full mass used in the metric iteration.

theorem OAI.RegularPointCoordinates.FirstOrderSplittingOn.closed_error_le line 25

Source documentation

Restricting the averaged error on the large harmonic ball controls the unnormalized error on every closed interior ball.

theorem FirstOrderSplittingOn.closed_error_le {n : ℕ} {p : X} {r ε R : ℝ}
    {u : Fin n → SobolevSpace μ hQ} {w : X → Euclidean n}
    (h : FirstOrderSplittingOn μ hQ p r ε u w) (hR : R < r)
    (hvol : 0 < μ.real (ball p r)) (hfinite : μ (ball p r) ≠ ∞) (i j : Fin n) :
    (∫ x in closedBall p R,
      |localGamma μ hQ (u i) (u j) x - (if i = j then 1 else 0)| ∂μ) ≤
      ε * μ.real (ball p r) := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.localGamma

theorem OAI.RegularPointCoordinates.splitting_normalized_bochner_mass_le line 46

Source documentation

The normalized full Bochner mass is small when the splitting error and the rescaled curvature are small.

theorem splitting_normalized_bochner_mass_le [IsFiniteMeasureOnCompacts μ]
    {n : ℕ} {p : X} {r ε C κ : ℝ} {L : ℝ≥0}
    {u : Fin n → SobolevSpace μ hQ} {w : X → Euclidean n}
    (h : FirstOrderSplittingOn μ hQ p (8 * r) ε u w)
    (hr : 0 < r) (hε : 0 ≤ ε) (hC : 0 ≤ C) (hκ : 0 ≤ κ)
    (hvol : 0 < μ.real (ball p (8 * r)))
    (χ : GoodLaplacianCutoff μ hQ p (r / 2) C)
    (M : PositiveBilinearMeasure X (Euclidean n))
    (G : ∀ v, LocalHarmonicEnergy μ hQ (sobolevColumnMap μ hQ u) M κ p r L v)
    (v : Euclidean n) :
    (r ^ 2 / μ.real (ball p (8 * r))) * ⟪v, M.massOperator (ball p (r / 2)) v⟫_ℝ ≤
      (2 * C * (n : ℝ) ^ 2 * ε + κ * r ^ 2 * ((n : ℝ) ^ 2 * ε + 1)) * ‖v‖ ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.sobolevColumnMap