OAI/Geometry/RCD/Sobolev/ScaledCutoffPairings.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.quadratic_norm_bound line 15
2. theorem OAI.RegularPointCoordinates.polarized_norm_of_tests line 22
3. theorem OAI.RegularPointCoordinates.exists_scaled_cutoff_pairing_bound line 41

   Source documentation

   Both scalar pairings have constants fixed before the radius and the actual harmonic map. The input L1 bound is proved for that map separately.

   theorem exists_scaled_cutoff_pairing_bound (n : ℕ) (hg : HasCoordinateHeatBounds μ ker)
       (hdiff : HasGaussianHeatDifferenceBounds μ ker)
       {A V c B : ℝ} (hA : 0 ≤ A) (hV : 0 < V) (hc : 0 < c) (hB : 0 ≤ B) :
       ∃ C : ℝ, 0 < C ∧ ∀ (R : ℝ), 0 < R →
         ∀ (U : Euclidean n →L[ℝ] SobolevSpace μ hQ) (M : PositiveBilinearMeasure X (Euclidean n))
           (κ r₀ : ℝ) (p : X) (L : ℝ≥0)
           (G : ∀ v, LocalHarmonicEnergy μ hQ U M κ p r₀ L v)
           (ρ C₀ : ℝ) (χ : GoodLaplacianCutoff μ hQ p ρ C₀),
         0 < ρ → ρ < r₀ →
         (∀ w : Euclidean n, ‖w‖ ≤ 2 → R ^ 2 *
           (∫ z, |cutoffSourceDensity μ hQ (G w).energy χ.sobolev χ.laplacian z| ∂μ) ≤ B * R ^ n) →
         ∀ (r t : ℝ) (x q : X), 0 < r → r ≤ 1 → 0 < t → t ≤ 1 →
   …

   Mentions: OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.HasGaussianHeatDifferenceBounds, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.cutoffSourceDensity