ScalarDimensionalBochner.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The scalar finite-dimensional Bochner inequality and its measure form

Han, JGA 28 (2018), Theorem 3.3, gives the scalar Bakry--Émery inequality on compact Lipschitz functions with L² Laplacian. The finite-family measure identities use the full positive regular Bochner measure.

def OAI.RegularPointCoordinates.ScalarDimensionalBochner line 25
Source documentation
The scalar weak BE(K,N) inequality on the compact regular class used in this application. The mixed source is interpreted by the actual weak Laplacian; no Sobolev derivative of that source is required.
```
def ScalarDimensionalBochner (K N : ℝ) : Prop :=
…
```

theorem OAI.RegularPointCoordinates.ScalarDimensionalBochner.regular_form line 40

Source documentation

The scalar test formula is exactly the diagonal of the existing bilinear Bochner form, including its L² source terms.

theorem ScalarDimensionalBochner.regular_form {K N : ℝ}
    (h : ScalarDimensionalBochner μ hQ K N) {m : ℕ}
    (U : Euclidean m →L[ℝ] SobolevSpace μ hQ)
    (D : Euclidean m →L[ℝ] Lp ℝ 2 μ)
    (H : Euclidean m →ₗ[ℝ] Euclidean m →ₗ[ℝ] SobolevSpace μ hQ)
    (L : Euclidean m → ℝ≥0)
    (hU : ∀ a, ∀ᵐ x ∂μ, SobolevSpace.minimalSlope μ hQ (U a) x≤L a)
    (hc : ∀ a, ∃ (v : X → ℝ) (A : ℝ≥0), LipschitzWith A v ∧
      HasCompactSupport v ∧ SobolevSpace.toLp μ hQ (U a) =ᵐ[μ] v)
    (hD : ∀ a, IsWeakLaplacian μ hQ (U a) (D a))
    (hH : ∀ a, SobolevSpace.toLp μ hQ (H a a) =ᵐ[μ] localGamma μ hQ (U a) (U a))
    (a : Euclidean m) (q : X →ᵇ ℝ) (ψ : SobolevSpace μ hQ) (A : ℝ≥0)
…

Mentions: OAI.RegularPointCoordinates.ScalarDimensionalBochner, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.IsWeakLaplacian, OAI.RegularPointCoordinates.localGamma

theorem OAI.RegularPointCoordinates.ScalarDimensionalBochner.regular_density line 64

Source documentation

Scalar weak BE identifies the dimensional density of the actual full bilinear measure on every compact interior set.

theorem ScalarDimensionalBochner.regular_density [SigmaFinite μ] [SecondCountableTopology X]
    [IsFiniteMeasureOnCompacts μ] {K N : ℝ} (h : ScalarDimensionalBochner μ hQ K N)
    {m : ℕ} (U : Euclidean m →L[ℝ] SobolevSpace μ hQ)
    (D : Euclidean m →L[ℝ] Lp ℝ 2 μ)
    (H : Euclidean m →ₗ[ℝ] Euclidean m →ₗ[ℝ] SobolevSpace μ hQ)
    (L : Euclidean m → ℝ≥0)
    (hU : ∀ a, ∀ᵐ x ∂μ, SobolevSpace.minimalSlope μ hQ (U a) x≤L a)
    (hc : ∀ a, ∃ (v : X → ℝ) (A : ℝ≥0), LipschitzWith A v ∧
      HasCompactSupport v ∧ SobolevSpace.toLp μ hQ (U a) =ᵐ[μ] v)
    (hD : ∀ a, IsWeakLaplacian μ hQ (U a) (D a))
    (hH : ∀ a, SobolevSpace.toLp μ hQ (H a a) =ᵐ[μ] localGamma μ hQ (U a) (U a))
    {Ω S : Set X} (M : PositiveBilinearMeasure X (Euclidean m))
…