BochnerCurvatureDensity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Comparison of Bochner densities under a lower curvature parameter

theorem OAI.RegularPointCoordinates.signed_rnDeriv_two_add_density line 15

theorem OAI.RegularPointCoordinates.bochnerDensity_curvature_le line 30

Source documentation

Decreasing the curvature parameter increases the Bochner density. This compares the actual full local sources before passing to densities.

theorem bochnerDensity_curvature_le {Ω S : Set X} (hΩ : MeasurableSet Ω)
    (hS : MeasurableSet S) {J K : ℝ} (hJK : J≤K)
    (f d F G : SobolevSpace μ hQ) (ν τ : Measure X) [IsFiniteMeasure ν] [IsFiniteMeasure τ]
    (hF : IsMeasureLaplacianOn μ hQ Ω F (bochnerGramSource μ hQ K f f d d ν.toSignedMeasure))
    (hG : IsMeasureLaplacianOn μ hQ Ω G (bochnerGramSource μ hQ J f f d d τ.toSignedMeasure))
    (hFG : SobolevSpace.toLp μ hQ F =ᵐ[μ.restrict Ω] SobolevSpace.toLp μ hQ G)
    (χ : X →ᵇ ℝ) {L : ℝ≥0} (hχ : LipschitzWith L χ)
    (hχc : HasCompactSupport (χ : X → ℝ)) (hχΩ : tsupport χ ⊆ Ω)
    (hχ0 : ∀ x, 0≤χ x) (hχ1 : ∀ x ∈ S, χ x=1) :
    ∀ᵐ x ∂μ.restrict S, (ν.rnDeriv μ x).toReal≤(τ.rnDeriv μ x).toReal := by
…

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