RegularCenterRadialData.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Actual radial data at every center of the common heat neighborhood

structure OAI.RegularPointCoordinates.RegularCenterRadialData line 17

Source documentation

Sources, normalizing frames and radial fits all use the same harmonic map.

structure RegularCenterRadialData {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X)
    [(hausdorff n X).Regular]
    {p : X} {ker : ℝ → X → X → ℝ}
    {hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker}
    {enlargement zeta : ℝ} (heat : RegularBilinearData hX p hk enlargement zeta)
    (κ B J C A Cχ eta Cg D Ca : ℝ) (q : X) where
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularBilinearData

theorem OAI.RegularPointCoordinates.regular_center_radial_constants line 50

Source documentation

Uniform radial constants can be chosen before any neighborhood or error size. This uses the proved radial estimates and the fixed heat degree.

theorem regular_center_radial_constants {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 2) X) [(hausdorff (m + 2) X).Regular]
    (hhessian : LocalPoissonHessianInput hX) (hmean : LocalHarmonicL2MeanValueInput hX)
    (hgradient : LocalHarmonicL2GradientInput hX)
    {B J A Cχ : ℝ} {degree : ℕ} (hB : 0 ≤ B) (hJ : 0 ≤ J) (hA : 0 ≤ A)
    (hCχ : 0 ≤ Cχ) (hdegree : 0 < degree) :
    ∃ Cg D Ca : ℝ, 1 ≤ Cg ∧ 0 < D ∧ 1 ≤ Ca ∧
    ∀ {p : X} {a κ C enlargement zeta eta : ℝ}
      {ker : ℝ → X → X → ℝ}
      {hk : IsContinuousHeatKernel (hausdorff (m + 2) X) hX.quadratic ker},
      0 ≤ a → 0 ≤ κ → -κ ≤ K → 0 ≤ zeta →
      radialNormalizationRestrictionConstant (m + 2) * zeta ≤ 1 →
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalPoissonHessianInput, OAI.RegularPointCoordinates.LocalHarmonicL2MeanValueInput, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.radialNormalizationRestrictionConstant