ShiftedBochnerCutoff.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The shifted Poisson mass estimate from the actual local equations

theorem OAI.RegularPointCoordinates.IsMeasureLaplacianOn.test_positive_defect line 23

Source documentation

The weak equation for a full signed Laplacian gives the defect identity against an actual Sobolev cutoff.

theorem IsMeasureLaplacianOn.test_positive_defect
    {S : Set X} [IsFiniteMeasure (μ.restrict S)]
    (Q : SobolevSpace μ hQ) (a : ℝ) (σ : Measure X) [IsFiniteMeasure σ]
    (hQsource : IsMeasureLaplacianOn μ hQ S Q
      (a • (μ.restrict S).toSignedMeasure - σ.toSignedMeasure))
    (χ : X →ᵇ ℝ) (hχs : HasCompactSupport (χ : X → ℝ))
    (hχS : tsupport (χ : X → ℝ) ⊆ S)
    (c : SobolevSpace μ hQ) (hc : SobolevSpace.toLp μ hQ c =ᵐ[μ] χ)
    (q : Lp ℝ 2 μ) (hq : IsWeakLaplacian μ hQ c q)
    (hqs : ∀ᵐ x ∂μ, x ∉ S → q x = 0) :
    (∫ x in S, SobolevSpace.toLp μ hQ Q x * q x ∂μ) =
      a * (∫ x in S, χ x ∂μ) - ∫ x, χ x ∂σ := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsMeasureLaplacianOn, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.IsWeakLaplacian

theorem OAI.RegularPointCoordinates.LocalHarmonicEnergy.test_shifted_cutoff line 62

Source documentation

The shifted measure satisfies the exact cutoff identity, including the trace correction and its full singular mass.

theorem LocalHarmonicEnergy.test_shifted_cutoff
    {U : E →L[ℝ] SobolevSpace μ hQ} {M : PositiveBilinearMeasure X E}
    {κ : ℝ} {p : X} {r : ℝ} {L : ℝ≥0} {v : E}
    [IsFiniteMeasure (μ.restrict (ball p (2 * r)))]
    (G : LocalHarmonicEnergy μ hQ U M κ p r L v)
    (ell : E →ₗ[ℝ] ℝ) (n b : ℝ)
    (hshift : ShiftedBochnerLowerBound M (μ.restrict (ball p (2 * r))) ell n)
    (χ : X →ᵇ ℝ) (hχs : HasCompactSupport (χ : X → ℝ))
    (hχS : tsupport (χ : X → ℝ) ⊆ ball p (2 * r))
    (c : SobolevSpace μ hQ) (hc : SobolevSpace.toLp μ hQ c =ᵐ[μ] χ)
    (q : Lp ℝ 2 μ) (hq : IsWeakLaplacian μ hQ c q)
    (hqs : ∀ᵐ x ∂μ, x ∉ ball p (2 * r) → q x = 0) :
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.ShiftedBochnerLowerBound, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.IsWeakLaplacian

theorem OAI.RegularPointCoordinates.shifted_poisson_bochner_mass_le line 98

Source documentation

Both raw source identities in the shifted Bochner estimate follow from the local PDEs and the cutoff Laplacian.

theorem shifted_poisson_bochner_mass_le
    {U : E →L[ℝ] SobolevSpace μ hQ} {M : PositiveBilinearMeasure X E}
    {κ : ℝ} {p : X} {r : ℝ} {L : ℝ≥0} {v : E}
    [IsFiniteMeasure (μ.restrict (ball p (2 * r)))]
    (G : LocalHarmonicEnergy μ hQ U M κ p r L v)
    (ell : E →ₗ[ℝ] ℝ) (n : ℝ)
    (hshift : ShiftedBochnerLowerBound M (μ.restrict (ball p (2 * r))) ell n)
    (Q : SobolevSpace μ hQ) (σ : Measure X) [IsFiniteMeasure σ]
    (hQsource : IsMeasureLaplacianOn μ hQ (ball p (2 * r)) Q
      (ell v • (μ.restrict (ball p (2 * r))).toSignedMeasure - σ.toSignedMeasure))
    (χ : X →ᵇ ℝ) (hχ : ∀ x, 0 ≤ χ x ∧ χ x ≤ 1)
    (hχs : HasCompactSupport (χ : X → ℝ))
…