HarmonicBochnerMass.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Small Bochner mass from the harmonic Gram error

The local harmonic Bochner equation and cutoff Laplacian bound the full measure.

theorem OAI.RegularPointCoordinates.harmonic_bochner_mass_le line 24

Source documentation

The canonical local Bochner family satisfies the small-mass estimate with exactly the dimension loss in the coordinatewise Gram error.

theorem harmonic_bochner_mass_le {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (M : PositiveBilinearMeasure X (Euclidean n)) {κ : ℝ} {p : X} {r : ℝ} {L : ℝ≥0}
    (G : ∀ v, LocalHarmonicEnergy μ hQ (sobolevColumnMap μ hQ u) M κ p r L v)
    (χ : X →ᵇ ℝ) (hχ : ∀ x, 0 ≤ χ x ∧ χ x ≤ 1)
    (hχs : HasCompactSupport (χ : X → ℝ))
    (hχΩ : tsupport (χ : X → ℝ) ⊆ ball p (2 * r))
    {R : ℝ} (hR : 0 < R) (hRr : R < 2 * r)
    (hχR : ∀ x, R < dist p x → χ x = 0)
    (c : SobolevSpace μ hQ) (hc : SobolevSpace.toLp μ hQ c =ᵐ[μ] χ)
    (q : Lp ℝ 2 μ) (hq : IsWeakLaplacian μ hQ c q)
    (hqR : ∀ᵐ x ∂μ, R < dist p x → q x = 0)
    (s : Set X) (hs : MeasurableSet s) (hχone : ∀ x ∈ s, χ x = 1)
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.IsWeakLaplacian