AnalyticLpCalculus.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform estimates in the concrete Hilbert space

The restricted Lebesgue measure has mass one. Consequently, an almost-everywhere uniform bound on a representative gives the same bound on its L² norm. The derivative criterion below turns a quadratic norm remainder into a genuine derivative in any real normed space, including this Hilbert space.

theorem OAI.ThompsonNonamenability.Analytic.intervalMeasure_univ line 24
theorem OAI.ThompsonNonamenability.Analytic.norm_le_of_ae_bound line 28
Source documentation
A uniform bound on an almost-everywhere representative bounds the Hilbert norm.
```
theorem norm_le_of_ae_bound (f : Hilbert) {C : ℝ} (hC : 0 ≤ C)
    (hbound : ∀ᵐ x ∂intervalMeasure, ‖f x‖ ≤ C) : ‖f‖ ≤ C := by
…
```
Mentions: OAI.ThompsonNonamenability.Analytic.Hilbert, OAI.ThompsonNonamenability.Analytic.intervalMeasure
theorem OAI.ThompsonNonamenability.Analytic.norm_toLp_le line 38
Source documentation
The same estimate for an explicitly supplied square-integrable function.
```
theorem norm_toLp_le {f : ℝ → Plane} (hf : MemLp f 2 intervalMeasure)
    {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ᵐ x ∂intervalMeasure, ‖f x‖ ≤ C) :
    ‖hf.toLp f‖ ≤ C := by
…
```
Mentions: OAI.ThompsonNonamenability.Analytic.Plane, OAI.ThompsonNonamenability.Analytic.intervalMeasure

theorem OAI.ThompsonNonamenability.Analytic.hasDerivAt_of_quadratic_remainder line 47

Source documentation

A quadratic norm remainder implies differentiability, without any pointwise choice of representatives in the codomain.

theorem hasDerivAt_of_quadratic_remainder
    {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {f : ℝ → E} {f' : E} {x C : ℝ}
    (hrem : ∀ᶠ h in 𝓝 (0 : ℝ),
      ‖f (x + h) - f x - h • f'‖ ≤ C * |h| ^ 2) :
    HasDerivAt f f' x := by
…