AveragedCutoffError.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exact quadratic identities for the averaged cutoff error

theorem OAI.RegularPointCoordinates.GoodLaplacianCutoff.error_zero_off_outerBall line 19
Source documentation
The actual product-rule source is supported in the closed outer ball.
```
theorem GoodLaplacianCutoff.error_zero_off_outerBall {p : X} {ρ C : ℝ}
    (χ : GoodLaplacianCutoff μ hQ p ρ C) (u : SobolevSpace μ hQ) :
    ∀ᵐ z ∂μ, z ∉ closedBall p (2 * ρ) →
      cutoffSourceDensity μ hQ u χ.sobolev χ.laplacian z = 0 := by
…
```
Mentions: OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.cutoffSourceDensity

theorem OAI.RegularPointCoordinates.averaged_cutoff_error_energy line 38

Source documentation

The averaged error is quadratic in every direction; this follows from the actual pointwise heat equation and Fubini, not an extra quadraticity input.

theorem averaged_cutoff_error_energy (hρ : 0 < ρ) (hρr : ρ < r)
    {t : ℝ} (ht : 0 < t) (A : Set X) (hA : MeasurableSet A)
    (hbounded : Bornology.IsBounded A) (v : Euclidean n) :
    ⟪v, polarizedDerivative (fun w => ∫ z, kernelAverage μ ker t A z *
      cutoffSourceDensity μ hQ (G w).energy χ.sobolev χ.laplacian z ∂μ) v⟫_ℝ =
      ∫ z, kernelAverage μ ker t A z *
        cutoffSourceDensity μ hQ (G v).energy χ.sobolev χ.laplacian z ∂μ := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.polarizedDerivative, OAI.RegularPointCoordinates.kernelAverage, OAI.RegularPointCoordinates.cutoffSourceDensity

theorem OAI.RegularPointCoordinates.difference_cutoff_error_energy line 72

Source documentation

The averaged-minus-pointwise source pairing is likewise the quadratic form of its finite polarization.

theorem difference_cutoff_error_energy (hρ : 0 < ρ) (hρr : ρ < r)
    {t : ℝ} (ht : 0 < t) (A : Set X) (hA : MeasurableSet A)
    (hbounded : Bornology.IsBounded A) (x : X) (v : Euclidean n) :
    ⟪v, polarizedDerivative (fun w => ∫ z, (kernelAverage μ ker t A z - ker t x z) *
      cutoffSourceDensity μ hQ (G w).energy χ.sobolev χ.laplacian z ∂μ) v⟫_ℝ =
      ∫ z, (kernelAverage μ ker t A z - ker t x z) *
        cutoffSourceDensity μ hQ (G v).energy χ.sobolev χ.laplacian z ∂μ := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.polarizedDerivative, OAI.RegularPointCoordinates.kernelAverage, OAI.RegularPointCoordinates.cutoffSourceDensity