RegularProjectionRows.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Actual radial rows in the coordinates used by sharp projection

def OAI.RegularPointCoordinates.projectionRowConstant line 17
theorem OAI.RegularPointCoordinates.projectionRowConstant_nonneg line 22

theorem OAI.RegularPointCoordinates.regular_center_projection_rows line 30

Source documentation

The same exact frames and local constant turn the radial rows into centered projection rows on the smaller ball, with a uniform coefficient.

theorem regular_center_projection_rows {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
    {p q : X} {ker : ℝ → X → X → ℝ}
    {hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker}
    {a κ B J C A Cχ enlargement zeta eta Cg D Ca : ℝ}
    (e : RegularProjectionEnvironment hX p hk a κ B J C A Cχ enlargement zeta eta)
    (hq : q ∈ ball p (e.heat.radius / 32))
    (d : RegularCenterRadialData hX e.heat κ B J C A Cχ eta Cg D Ca q)
    (hκ : 0 ≤ κ) (hB : 0 ≤ B) (hCχ : 0 ≤ Cχ) (hzeta : 0 ≤ zeta) (i : ℕ) :
    let s := distanceSourceRadius e.heat.radius i
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularProjectionEnvironment, OAI.RegularPointCoordinates.RegularCenterRadialData, OAI.RegularPointCoordinates.distanceSourceRadius