MeanGradient.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Averaging gradients against normalized Sobolev coordinates

def OAI.RegularPointCoordinates.meanGradientVector line 22
Source documentation
The vector of mean gradient pairings with the coordinate columns. It is defined using the canonical Sobolev Gram, not chosen coefficients.
```
def meanGradientVector : SobolevSpace μ hQ →L[ℝ] E :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace
theorem OAI.RegularPointCoordinates.meanGradientVector_inner line 26
theorem OAI.RegularPointCoordinates.meanGradientVector_column line 33
theorem OAI.RegularPointCoordinates.meanGradientVector_norm_sq_le line 41
Source documentation
Bessel's inequality for gradients in exactly normalized coordinates. The right side is the actual averaged local Cheeger energy of f.
```
theorem meanGradientVector_norm_sq_le
    (hnormal : sobolevMeanGram μ hQ U s hs = ContinuousLinearMap.id ℝ E)
    (f : SobolevSpace μ hQ) :
    ‖meanGradientVector μ hQ U s hs f‖ ^ 2 ≤
      (μ.real s)⁻¹ * ∫ x in s, (SobolevSpace.minimalSlope μ hQ f x) ^ 2 ∂μ := by
…
```
Mentions: OAI.RegularPointCoordinates.sobolevMeanGram, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.meanGradientVector, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope
theorem OAI.RegularPointCoordinates.meanGradientVector_coefficient_error line 77
Source documentation
Averaging the gradient of a fitted function recovers its linear coefficient, with an error bounded by the residual energy.
```
theorem meanGradientVector_coefficient_error
    (hnormal : sobolevMeanGram μ hQ U s hs = ContinuousLinearMap.id ℝ E)
    (f : SobolevSpace μ hQ) (b : E) :
    ‖meanGradientVector μ hQ U s hs f - b‖ ^ 2 ≤
      (μ.real s)⁻¹ * ∫ x in s,
        (SobolevSpace.minimalSlope μ hQ (f - U b) x) ^ 2 ∂μ := by
…
```
Mentions: OAI.RegularPointCoordinates.sobolevMeanGram, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.meanGradientVector, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope