OAI/Geometry/RCD/Coordinates/RegularBochnerSquare.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.regularGram_abs_le line 18
2. theorem OAI.RegularPointCoordinates.regularBochner_square_product line 35

   Source documentation

   Squaring one member of the regular family produces the actual full measure product identity. Only local Sobolev representatives of the two original Laplacians are needed.

   theorem regularBochner_square_product [μ.Regular] [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