OAI/Geometry/RCD/Sobolev/WeightedGammaL2Algebra.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.weightedGamma_lp_add_weight line 17
2. theorem OAI.RegularPointCoordinates.weightedGamma_lp_smul_weight line 31
3. theorem OAI.RegularPointCoordinates.weightedGamma_lp_add_left line 41
4. theorem OAI.RegularPointCoordinates.weightedGamma_lp_diagonal_add line 57

   Source documentation

   The full mixed source of two regular directions is symmetric after polarization; this expansion retains L² Laplacians without requiring bounded Laplacians.

   theorem weightedGamma_lp_diagonal_add (d e : Lp ℝ 2 μ) (f g w : SobolevSpace μ hQ)
       (L M : ℝ≥0)
       (hf : ∀ᵐ x ∂μ, SobolevSpace.minimalSlope μ hQ f x≤L)
       (hg : ∀ᵐ x ∂μ, SobolevSpace.minimalSlope μ hQ g x≤M) :
       weightedGamma μ hQ (d+e : Lp ℝ 2 μ) (f+g) w =
         weightedGamma μ hQ d f w+weightedGamma μ hQ d g w+
         weightedGamma μ hQ e f w+weightedGamma μ hQ e g w := by
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope, OAI.RegularPointCoordinates.weightedGamma