LocalL2Restriction.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Restricting actual local L² functions between the fitting balls

def OAI.RegularPointCoordinates.localL2Restriction line 16
Source documentation
Restriction to a smaller measurable region as a continuous linear map.
```
def localL2Restriction (s t : Set X) (hts : t ⊆ s) :
    Lp ℝ 2 (μ.restrict s) →L[ℝ] Lp ℝ 2 (μ.restrict t) :=
…
```
theorem OAI.RegularPointCoordinates.localL2Restriction_coe line 22
theorem OAI.RegularPointCoordinates.localL2Restriction_norm_le line 28
theorem OAI.RegularPointCoordinates.localL2Restriction_sobolev line 38
theorem OAI.RegularPointCoordinates.restrictedOne_coe line 48
theorem OAI.RegularPointCoordinates.localL2Restriction_one line 56
theorem OAI.RegularPointCoordinates.localL2Restriction_affine line 64

theorem OAI.RegularPointCoordinates.normalized_localL2Restriction_le line 75

Source documentation

The only norm loss under normalized restriction is the square root of the volume ratio, written as a ratio of the actual constant-function norms.

theorem normalized_localL2Restriction_le (s t : Set X) (hts : t ⊆ s)
    (hs : μ s ≠ ∞) (ht : μ t ≠ ∞) (hs0 : μ s ≠ 0) (ht0 : μ t ≠ 0)
    (f : Lp ℝ 2 (μ.restrict s)) :
    ‖normalizeLocalL2 μ t ht (localL2Restriction μ s t hts f)‖ ≤
      (Real.sqrt (μ.real s) / Real.sqrt (μ.real t)) * ‖normalizeLocalL2 μ s hs f‖ := by
…

Mentions: OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.localL2Restriction