BoundedLpSquare.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

L² continuity of squares on uniformly bounded sets

The heat-variance differentiation needs the square to remain in L² while the underlying bounded heat path varies in L².

def OAI.RegularPointCoordinates.boundedLpSquare line 20
Source documentation
The square of a bounded L² function is again an actual L² function.
```
def boundedLpSquare (f : Lp ℝ 2 μ) (C : ℝ) (_hC : 0 ≤ C)
    (hf : ∀ᵐ x ∂μ, |f x| ≤ C) : Lp ℝ 2 μ :=
…
```
theorem OAI.RegularPointCoordinates.boundedLpSquare_coe line 31

theorem OAI.RegularPointCoordinates.boundedLpSquare_sub_norm_le line 39

Source documentation

A quantitative continuity estimate requiring only L² distance and separate bounds on the two functions.

theorem boundedLpSquare_sub_norm_le (f g : Lp ℝ 2 μ) (C D : ℝ) (hC : 0 ≤ C) (hD : 0 ≤ D)
    (hf : ∀ᵐ x ∂μ, |f x| ≤ C) (hg : ∀ᵐ x ∂μ, |g x| ≤ D) :
    ‖boundedLpSquare μ f C hC hf-boundedLpSquare μ g D hD hg‖ ≤ (C+D)*‖f-g‖ := by
…

Mentions: OAI.RegularPointCoordinates.boundedLpSquare

theorem OAI.RegularPointCoordinates.boundedLpSquare_continuousAt line 58

Source documentation

Uniform boundedness makes squaring continuous along an L² path.

theorem boundedLpSquare_continuousAt {F : ℝ → Lp ℝ 2 μ} {t C : ℝ} (hC : 0 ≤ C)
    (hF : ContinuousAt F t) (hb : ∀ s, ∀ᵐ x ∂μ, |F s x| ≤ C) :
    ContinuousAt (fun s => boundedLpSquare μ (F s) C hC (hb s)) t := by
…

Mentions: OAI.RegularPointCoordinates.boundedLpSquare