NormalizedPoissonEulerGradient.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual Euler-gradient error in normalized defect units

def OAI.RegularPointCoordinates.poissonEulerGradientConstant line 17
Source documentation
The coefficient is independent of the center and scale.
```
def poissonEulerGradientConstant (n : ℕ) (A B J Cχ : ℝ) : ℝ :=
…
```

theorem OAI.RegularPointCoordinates.normalized_poisson_euler_gradient line 26

Source documentation

The actual gradient product rule gives a mean Euler-gradient error controlled by the two original summable defects, at every dyadic scale.

theorem normalized_poisson_euler_gradient {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [IsFiniteMeasureOnCompacts (hausdorff n X)]
    (hhessian : LocalPoissonHessianActionInput hX)
    (hproduct : LocalPoissonGradientProductInput hX)
    {κ B J C A Cχ epsilon r0 : ℝ} (hκ : 0 ≤ κ) (hK : -κ ≤ K)
    (hB : 0 ≤ B) (hJ : 0 ≤ J) (hCχ : 0 ≤ Cχ)
    (hA : 0 ≤ A) (hepsilon : 0 ≤ epsilon) (p₁ p₂ z : X)
    (S₁ : DyadicDistanceSources (hausdorff n X) hX.quadratic n κ p₁ r0)
    (S₂ : DyadicDistanceSources (hausdorff n X) hX.quadratic n κ p₂ r0)
    (T₁ : DyadicDistanceReplacements (hausdorff n X) hX.quadratic S₁ B J C)
    (T₂ : DyadicDistanceReplacements (hausdorff n X) hX.quadratic S₂ B J C)
    (i : ℕ)
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalPoissonHessianActionInput, OAI.RegularPointCoordinates.LocalPoissonGradientProductInput, OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements