OAI/Geometry/RCD/Sobolev/ScaledCutoffL1.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.harmonic_cutoff_scaled_L1 line 16
2. theorem OAI.RegularPointCoordinates.harmonic_cutoff_uniform_L1 line 75

   Source documentation

   One coefficient controls all unit coordinate tests and their pairwise sums.

   theorem harmonic_cutoff_uniform_L1 {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) [IsFiniteMeasureOnCompacts (hausdorff n X)]
       (hhessian : LocalPoissonHessianInput hX) (hproduct : LocalPoissonGradientProductInput hX)
       {p : X} {R κ C V B : ℝ} (hR : 0 < R) (hκ : 0 ≤ κ) (hK : -κ ≤ K)
       (hcurv : κ * R ^ 2 ≤ 1) (hC : 0 ≤ C) (hV : 0 ≤ V) (hB : 0 ≤ B)
       (L : ℝ≥0) (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic)
       (hu : ∀ i, IsSobolevHarmonicOn (hausdorff n X) hX.quadratic (ball p (32 * R)) (u i))
       (hgrad : ∀ v, ∀ᵐ x ∂(hausdorff n X).restrict (ball p (32 * R)),
         localGamma (hausdorff n X) hX.quadratic
           (sobolevColumnMap (hausdorff n X) hX.quadratic u v)
           (sobolevColumnMap (hausdorff n X) hX.quadratic u v) x ≤ (L : ℝ) ^ 2 * ‖v‖ ^ 2)
       {M : PositiveBilinearMeasure X (Euclidean n)}
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalPoissonHessianInput, OAI.RegularPointCoordinates.LocalPoissonGradientProductInput, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.Euclidean