RegularPairDirection.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Constant-direction recovery for the actual two-center replacements

def OAI.RegularPointCoordinates.regularRadialValueCoefficient line 15
Source documentation
The dimensionless value coefficient after restriction and frame transport.
```
def regularRadialValueCoefficient (n : ℕ) (B D : ℝ) : ℝ :=
…
```
def OAI.RegularPointCoordinates.regularRadialEnergyCoefficient line 21
Source documentation
The dimensionless energy coefficient for the same transported residual.
```
def regularRadialEnergyCoefficient (K : ℝ) (n : ℕ) (Cg A B J Cχ D : ℝ) : ℝ :=
…
```

theorem OAI.RegularPointCoordinates.regular_pair_direction line 32

Source documentation

The pairing is constructed from the actual radial derivatives. Every smallness premise here is an explicit scalar bound on the already constructed source envelopes; no direction or mass estimate is assumed.

theorem regular_pair_direction {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
    (haction : LocalPoissonHessianActionInput hX)
    (hgradient : LocalHarmonicL2GradientInput hX)
    (hmean : LocalHarmonicL2MeanValueInput hX) (hn : 2 ≤ n)
    {κ : ℝ} (hκ : 0 ≤ κ) :
    ∃ Cgrad Cmean : ℝ, 1 ≤ Cgrad ∧ 1 ≤ Cmean ∧
    ∀ {base first center : X} {a B J C A Cχ enlargement zeta eta Cg D Ca : ℝ}
      {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)
      (_hfirst : first ∈ ball base (e.heat.radius / 32))
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalPoissonHessianActionInput, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.LocalHarmonicL2MeanValueInput, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularProjectionEnvironment