OAI/Geometry/RCD/Coordinates/RegularPatchCumulative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.central_comparison_rescale line 14

   Source documentation

   A positive rescaling of the central mass changes only the finite constant.

   theorem central_comparison_rescale {H t mass T c : ℝ}
       (ht : 0 ≤ t) (hm : 0 ≤ mass) (hT : 0 ≤ T) (hc : 0 < c)
       (h : H ≤ T * (t + mass)) :
       H ≤ (T * (1 + c⁻¹)) * (t + c * mass) := by
   …

2. theorem OAI.RegularPointCoordinates.regular_patch_cumulative_comparison line 33

   Source documentation

   Actual raw masses, mean inverses and a strictly interior central heat scale satisfy both cumulative comparisons. All matrix changes and the reverse covering are derived from the constructed data.

   theorem regular_patch_cumulative_comparison {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
       {base : X} {a κ B J C A Cχ enlargement zeta eta : ℝ}
       {ker : ℝ → X → X → ℝ}
       {hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker}
       (e : RegularProjectionEnvironment hX base hk a κ B J C A Cχ enlargement zeta eta)
       (hzeta : 0 ≤ zeta) (hzeta1 : zeta ≤ 1) (hCχ : 0 ≤ Cχ)
       (hsmall : (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * ((1 / 8 : ℝ) ^ n)⁻¹) * zeta) ≤ 1 / 2)
       (hnear : (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * ((1 / 2 : ℝ) ^ n)⁻¹) * zeta) ≤ 1 / 4)
       (N : ℕ) :
       ∃ Theta tau : ℝ, 0 < Theta ∧ 0 < tau ∧ ∀ epsilon : ℝ, 0 ≤ epsilon → epsilon ≤ tau →
       (∀ i, 4 * pinchingMassUnitFactor n * regularSmallMassCoefficient n Cχ *
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularProjectionEnvironment, OAI.RegularPointCoordinates.tau, OAI.RegularPointCoordinates.pinchingMassUnitFactor, OAI.RegularPointCoordinates.regularSmallMassCoefficient