DimensionalBochnerTest.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Recovering the dimensional density from the weak Bochner test inequality

The only analytic input here is the scalar finite-dimensional Bochner test inequality, as in Han, JGA 28 (2018), Theorem 3.3. The proof identifies its absolutely continuous density while retaining the full positive measure.

theorem OAI.RegularPointCoordinates.signed_rnDeriv_nonneg_of_nonneg line 25
Source documentation
A nonnegative finite signed measure has nonnegative density.
```
theorem signed_rnDeriv_nonneg_of_nonneg (ν : SignedMeasure X) (hν : 0≤ν) :
    ∀ᵐ x ∂μ, 0≤ν.rnDeriv μ x := by
…
```

theorem OAI.RegularPointCoordinates.integral_dimensional_defect line 40

Source documentation

The test integral of the dimensional defect has its exact scalar form.

theorem integral_dimensional_defect (σ : Measure X) [IsFiniteMeasure σ]
    (d : Lp ℝ 2 μ) (N : ℝ) (q : X →ᵇ ℝ) :
    (∫ᵛ x, q x ∂<•(N • σ.toSignedMeasure-μ.withDensityᵥ (fun x => (d x)^2))) =
      N*(∫ x, q x ∂σ)-(∫ x, q x*(d x)^2 ∂μ) := by
…

theorem OAI.RegularPointCoordinates.dimensional_bochner_density_of_tests line 54

Source documentation

Weak tests give the scalar dimensional density inequality on a compact interior set. No absolute continuity of the full Bochner measure is used.

theorem dimensional_bochner_density_of_tests (σ : Measure X) [IsFiniteMeasure σ]
    (d : Lp ℝ 2 μ) (N : ℝ) {Ω S : Set X} (hS : MeasurableSet S)
    (χ : X →ᵇ ℝ) {L : ℝ≥0} (hχ : LipschitzWith L χ)
    (hχc : HasCompactSupport (χ : X → ℝ)) (hχΩ : tsupport χ ⊆ Ω)
    (hχ0 : 0≤χ) (hχ1 : ∀ x∈S, χ x=1)
    (htest : ∀ q : compactLipschitzTests Ω, 0≤(q : X →ᵇ ℝ) →
      (∫ x, (q : X →ᵇ ℝ) x*(d x)^2 ∂μ)≤N*(∫ x, (q : X →ᵇ ℝ) x ∂σ)) :
    ∀ᵐ x ∂μ.restrict S, (d x)^2≤N*(σ.rnDeriv μ x).toReal := by
…

Mentions: OAI.RegularPointCoordinates.compactLipschitzTests

theorem OAI.RegularPointCoordinates.dimensional_bilinear_density_of_tests line 91

Source documentation

The actual linear Laplacian map and common full bilinear measure therefore satisfy the pointwise finite-dimensional input used by the quadratic-perturbation theorem.

theorem dimensional_bilinear_density_of_tests {m : ℕ}
    (M : PositiveBilinearMeasure X (Euclidean m)) (D : Euclidean m →L[ℝ] Lp ℝ 2 μ)
    (N : ℝ) {Ω S : Set X} (hS : MeasurableSet S)
    (χ : X →ᵇ ℝ) {L : ℝ≥0} (hχ : LipschitzWith L χ)
    (hχc : HasCompactSupport (χ : X → ℝ)) (hχΩ : tsupport χ ⊆ Ω)
    (hχ0 : 0≤χ) (hχ1 : ∀ x∈S, χ x=1)
    (htest : ∀ a (q : compactLipschitzTests Ω), 0≤(q : X →ᵇ ℝ) →
      (∫ x, (q : X →ᵇ ℝ) x*(D a x)^2 ∂μ)≤N*(∫ x, (q : X →ᵇ ℝ) x ∂M.measure a)) :
    ∀ a, ∀ᵐ x ∂μ.restrict S,
      (laplacianCoordinateForm μ D x a)^2≤N*bochnerRadonDensity μ M x a a := by
…

Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.compactLipschitzTests, OAI.RegularPointCoordinates.laplacianCoordinateForm, OAI.RegularPointCoordinates.bochnerRadonDensity