BochnerMassEstimate.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Small Bochner mass from the centered local Gram error

The weak Bochner identity and a cutoff bound the full positive measure. Subtracting the constant Gram field exposes the small normalized error.

theorem OAI.RegularPointCoordinates.bochner_mass_le_of_local_error line 28

Source documentation

Small normalized gradient error and small curvature force small full mass on every set where the test cutoff equals one.

theorem bochner_mass_le_of_local_error (U : E →L[ℝ] SobolevSpace μ hQ)
    (M : PositiveBilinearMeasure X E) (φ : X →ᵇ ℝ)
    (hφ : ∀ x, 0 ≤ φ x ∧ φ x ≤ 1)
    (S s : Set X) (hSfin : μ S ≠ ∞)
    (hs : MeasurableSet s) (hφone : ∀ x ∈ s, φ x = 1)
    (q : X → ℝ) {D epsilon kappa : ℝ} (hD : 0 ≤ D) (hk : 0 ≤ kappa)
    (hqmeas : AEStronglyMeasurable q (μ.restrict S))
    (hq : ∀ᵐ x ∂μ.restrict S, |q x| ≤ D)
    (hqzero : ∫ x in S, q x ∂μ = 0)
    (herror : ∀ v : E, ∫ x in S,
      |localGamma μ hQ (U v) (U v) x - ‖v‖ ^ 2| ∂μ ≤ epsilon * ‖v‖ ^ 2)
    (hsource : ∀ v : E,
…

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

theorem OAI.RegularPointCoordinates.bochner_mass_le_of_coordinate_errors line 100

Source documentation

Coordinatewise Gram errors suffice for the full mass estimate. The actual weak Laplacian of the compact cutoff supplies its zero integral, and finite-dimensional polarization supplies every direction.

theorem bochner_mass_le_of_coordinate_errors [IsFiniteMeasureOnCompacts μ]
    {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (M : PositiveBilinearMeasure X (Euclidean n)) (φ : X →ᵇ ℝ)
    (hφ : ∀ x, 0 ≤ φ x ∧ φ x ≤ 1) (p : X) {R : ℝ} (hR : 0 < R)
    (hφsupp : ∀ x, R < dist p x → φ x = 0)
    (ψ : SobolevSpace μ hQ) (hψ : SobolevSpace.toLp μ hQ ψ =ᵐ[μ] φ)
    (q : Lp ℝ 2 μ) (hd : IsWeakLaplacian μ hQ ψ q)
    (hqsupp : ∀ᵐ x ∂μ, R < dist p x → q x = 0)
    (s : Set X) (hs : MeasurableSet s) (hφone : ∀ x ∈ s, φ x = 1)
    {D epsilon kappa : ℝ} (hD : 0 ≤ D) (heps : 0 ≤ epsilon) (hk : 0 ≤ kappa)
    (hq : ∀ᵐ x ∂μ, |q x| ≤ D)
    (herror : ∀ i j : Fin n, ∫ x in Metric.closedBall p R,
…

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