BoundedLocalCoordinates.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Bounded Sobolev representatives preserving local harmonic coordinates

def OAI.RegularPointCoordinates.boundedLocalVersion line 18
Source documentation
Clipping only the global extension leaves a locally bounded coordinate unchanged.
```
def boundedLocalVersion (f : SobolevSpace μ hQ) (C : ℝ≥0) : SobolevSpace μ hQ :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace
theorem OAI.RegularPointCoordinates.boundedLocalVersion_bound line 21
theorem OAI.RegularPointCoordinates.boundedLocalVersion_eq line 30
theorem OAI.RegularPointCoordinates.IsSobolevHarmonicOn.congr_ae line 41
Source documentation
Harmonicity depends only on the local almost-everywhere representative.
```
theorem IsSobolevHarmonicOn.congr_ae {Ω : Set X} (hΩ : MeasurableSet Ω)
    {f g : SobolevSpace μ hQ} (hf : IsSobolevHarmonicOn μ hQ Ω f)
    (heq : SobolevSpace.toLp μ hQ g =ᵐ[μ.restrict Ω] SobolevSpace.toLp μ hQ f) :
    IsSobolevHarmonicOn μ hQ Ω g := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.SobolevSpace.toLp
theorem OAI.RegularPointCoordinates.boundedLocalVersion_harmonic line 54
theorem OAI.RegularPointCoordinates.boundedLocalVersion_gamma line 61

theorem OAI.RegularPointCoordinates.boundedLocalVersion_pair line 72

Source documentation

Replacing both slots preserves the actual local Gram matrix.

theorem boundedLocalVersion_pair {Ω : Set X} (f g : SobolevSpace μ hQ) (C D : ℝ≥0)
    (hf : ∀ᵐ x ∂μ.restrict Ω, |SobolevSpace.toLp μ hQ f x| ≤ C)
    (hg : ∀ᵐ x ∂μ.restrict Ω, |SobolevSpace.toLp μ hQ g x| ≤ D) :
    localGamma μ hQ (boundedLocalVersion μ hQ f C) (boundedLocalVersion μ hQ g D)
      =ᵐ[μ.restrict Ω] localGamma μ hQ f g := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.boundedLocalVersion