BochnerMassComparison.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Comparing two local realizations of the same Bochner energy

theorem OAI.RegularPointCoordinates.LocalHarmonicEnergy.cutoff_mass_eq line 22

Source documentation

Two local Bochner constructions have identical cutoff masses when their energy densities agree on the cutoff region. This also compares measures constructed on different finite dimensional spans.

theorem LocalHarmonicEnergy.cutoff_mass_eq
    {U : E →L[ℝ] SobolevSpace μ hQ} {V : F →L[ℝ] SobolevSpace μ hQ}
    {M : PositiveBilinearMeasure X E} {N : PositiveBilinearMeasure X F}
    {κ : ℝ} {p : X} {r ρ C : ℝ} {L H : ℝ≥0} {v : E} {w : F}
    (G : LocalHarmonicEnergy μ hQ U M κ p r L v)
    (G' : LocalHarmonicEnergy μ hQ V N κ p r H w)
    (χ : GoodLaplacianCutoff μ hQ p ρ C) (hρr : ρ < r)
    (heq : localGamma μ hQ (U v) (U v) =ᵐ[μ.restrict (ball p (2 * r))]
      localGamma μ hQ (V w) (V w)) :
    ⟪v, M.weightedOperator χ.weight v⟫_ℝ =
      ⟪w, N.weightedOperator χ.weight w⟫_ℝ := by
…

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

theorem OAI.RegularPointCoordinates.LocalHarmonicEnergy.mass_le_of_same_energy line 72

Source documentation

Positivity turns equality of the cutoff masses into comparison on nested balls. The full measures, including singular parts, are retained.

theorem LocalHarmonicEnergy.mass_le_of_same_energy
    {U : E →L[ℝ] SobolevSpace μ hQ} {V : F →L[ℝ] SobolevSpace μ hQ}
    {M : PositiveBilinearMeasure X E} {N : PositiveBilinearMeasure X F}
    {κ : ℝ} {p : X} {r ρ C : ℝ} {L H : ℝ≥0} {v : E} {w : F}
    (G : LocalHarmonicEnergy μ hQ U M κ p r L v)
    (G' : LocalHarmonicEnergy μ hQ V N κ p r H w)
    (χ : GoodLaplacianCutoff μ hQ p ρ C) (hρ : 0 < ρ) (hρr : ρ < r)
    (heq : localGamma μ hQ (U v) (U v) =ᵐ[μ.restrict (ball p (2 * r))]
      localGamma μ hQ (V w) (V w)) :
    ⟪v, M.massOperator (ball p ρ) v⟫_ℝ ≤
      ⟪w, N.massOperator (ball p (3 * ρ)) w⟫_ℝ := by
…