MeanDirectionFromPairings.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.RegularPointCoordinates.meanGradientVector_error_of_pairings line 23
Source documentation
The constant-direction L2 estimate controls the actual averaged coordinate gradient. This is the bridge from the two-center commutator estimate to coefficient recovery in directional pinching.
```
theorem meanGradientVector_error_of_pairings
    (U H : E →L[ℝ] SobolevSpace μ hQ) (f : SobolevSpace μ hQ)
    (s : Set X) (hs : MeasurableSet s) (hfin : μ s ≠ ∞) (hpos : μ s ≠ 0)
    (δ : E) {D : ℝ} (hD : 0 ≤ D)
    (hrep : ∀ b, SobolevSpace.toLp μ hQ (H b) =ᵐ[μ.restrict s]
      localGamma μ hQ f (U b))
    (herror : ∀ b, ‖normalizeLocalL2 μ s hfin
      (SobolevSpace.restrictLp μ hQ s (H b) - ⟪δ, b⟫_ℝ • restrictedOne μ s hfin)‖ ≤ D * ‖b‖) :
    ‖meanGradientVector μ hQ U s hs f - δ‖ ≤ D := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.restrictedOne, OAI.RegularPointCoordinates.meanGradientVector