OAI/Geometry/RCD/Coordinates/RegularBochnerDirectional.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.regularBochner_directional_bound line 20

   Source documentation

   The full product calculus and measure positivity give the sharp pointwise diagonal-direction Hessian bound, with the same Bochner measure.

   theorem regularBochner_directional_bound [μ.Regular] [SigmaFinite μ] [SecondCountableTopology X]
       (K : ℝ) (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)
       (hD : ∀ a, IsWeakLaplacian μ hQ (U a) (D a))
       (hH : ∀ a b, SobolevSpace.toLp μ hQ (H a b) =ᵐ[μ] localGamma μ hQ (U a) (U b))
       (hsym : ∀ a b, H a b=H b a)
       {Ω S : Set X} (hΩ : MeasurableSet Ω) (M : PositiveBilinearMeasure X (Euclidean m))
       (hM : ∀ (a : Euclidean m) (ψ : SobolevSpace μ hQ) (q : X →ᵇ ℝ),
         HasCompactSupport (q : X → ℝ) → tsupport q ⊆ Ω →
   …

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