PinchingFromProjection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

From a sharp projection to directional mass

The residual energy, constant-direction estimate and mass estimates are kept explicit. The coefficient-recovery step uses the actual normalized Sobolev Gram. The local Bochner estimates supplying the other hypotheses are not asserted here.

theorem OAI.RegularPointCoordinates.coefficient_recovery_sq line 30
Source documentation
The constant-direction error and the sharp projection energy control the difference between the true coordinate displacement and the fitted linear coefficient. All errors remain squared.
```
theorem coefficient_recovery_sq
    (hnormal : sobolevMeanGram μ hQ U s hs = ContinuousLinearMap.id ℝ E)
    (f : SobolevSpace μ hQ) (b δ : E) {e d : ℝ}
    (henergy : (μ.real s)⁻¹ * ∫ x in s,
      (SobolevSpace.minimalSlope μ hQ (f - U b) x) ^ 2 ∂μ ≤ e)
    (hdirection : ‖meanGradientVector μ hQ U s hs f - δ‖ ^ 2 ≤ d) :
    ‖δ - b‖ ^ 2 ≤ 2 * (d + e) := by
…
```
Mentions: OAI.RegularPointCoordinates.sobolevMeanGram, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope, OAI.RegularPointCoordinates.meanGradientVector

theorem OAI.RegularPointCoordinates.directional_mass_of_projection line 49

Source documentation

Transfer small mass from the fitted coefficient to the actual coordinate displacement. This also allows a singular local mass form.

theorem directional_mass_of_projection
    (hnormal : sobolevMeanGram μ hQ U s hs = ContinuousLinearMap.id ℝ E)
    (f : SobolevSpace μ hQ) (b δ : E) (D : E →L[ℝ] E)
    (hD : D.IsPositive) {e d m K : ℝ} (hK : 0 ≤ K)
    (henergy : (μ.real s)⁻¹ * ∫ x in s,
      (SobolevSpace.minimalSlope μ hQ (f - U b) x) ^ 2 ∂μ ≤ e)
    (hdirection : ‖meanGradientVector μ hQ U s hs f - δ‖ ^ 2 ≤ d)
    (hmass : ⟪b, D b⟫_ℝ ≤ m)
    (hupper : ∀ v, ⟪v, D v⟫_ℝ ≤ K * ‖v‖ ^ 2) :
    ⟪δ, D δ⟫_ℝ ≤ 2 * m + 4 * K * (d + e) := by
…

Mentions: OAI.RegularPointCoordinates.sobolevMeanGram, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope, OAI.RegularPointCoordinates.meanGradientVector