L^∞-normalized t-Hölder norm

This file defines the L^∞-normalized t-Hölder norm, which probably in some form should end up in Mathlib. Lemmas about this norm that are proven in Carleson are collected here.

TODO: Assess Mathlib-readiness, complete basic results, optimize imports.

noncomputable def iHolENorm {𝕜 : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [NormedField 𝕜] (φ : X → 𝕜) (x₀ : X) (R t : ℝ) : ENNReal

the L^∞-normalized t-Hölder norm. Defined in ℝ≥0∞ to avoid sup-related issues.

Equations

• iHolENorm φ x₀ R t = (⨆ x ∈ Metric.ball x₀ R, ‖φ x‖ₑ) + ENNReal.ofReal R ^ t * ⨆ x ∈ Metric.ball x₀ R, ⨆ y ∈ Metric.ball x₀ R, ⨆ (_ : x ≠ y), ‖φ x - φ y‖ₑ / edist x y ^ t

noncomputable def iHolNNNorm {𝕜 : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [NormedField 𝕜] (φ : X → 𝕜) (x₀ : X) (R t : ℝ) : NNReal

The NNReal version of the L^∞-normalized t-Hölder norm, iHolENorm.

Equations

• iHolNNNorm φ x₀ R t = (iHolENorm φ x₀ R t).toNNReal

theorem enorm_le_iHolENorm_of_mem {X : Type u_1} {𝕜 : Type u_2} {x z : X} {R t : ℝ} {φ : X → 𝕜} [MetricSpace X] [NormedField 𝕜] (hx : x ∈ Metric.ball z R) : ‖φ x‖ₑ ≤ iHolENorm φ z R t

theorem HolderOnWith.of_iHolENorm_ne_top {X : Type u_1} {𝕜 : Type u_2} {z : X} {R t : ℝ} {φ : X → 𝕜} [MetricSpace X] [NormedField 𝕜] (ht : 0 ≤ t) (hφ : iHolENorm φ z R t ≠ ⊤) : HolderOnWith (iHolNNNorm φ z R t / R.toNNReal ^ t) t.toNNReal φ (Metric.ball z R)

theorem continuous_of_iHolENorm_ne_top {X : Type u_1} {𝕜 : Type u_2} {z : X} {R t : ℝ} {φ : X → 𝕜} [MetricSpace X] [NormedField 𝕜] (ht : 0 < t) (hφ : tsupport φ ⊆ Metric.ball z R) (h'φ : iHolENorm φ z R t ≠ ⊤) : Continuous φ

theorem continuous_of_iHolENorm_ne_top' {X : Type u_1} {𝕜 : Type u_2} {z : X} {R t : ℝ} {φ : X → 𝕜} [MetricSpace X] [NormedField 𝕜] (ht : 0 < t) (hφ : Function.support φ ⊆ Metric.ball z R) (h'φ : iHolENorm φ z (2 * R) t ≠ ⊤) : Continuous φ

theorem norm_le_iHolNNNorm_of_mem {X : Type u_1} {𝕜 : Type u_2} {x z : X} {R t : ℝ} {φ : X → 𝕜} [MetricSpace X] [NormedField 𝕜] (hφ : iHolENorm φ z R t ≠ ⊤) (hx : x ∈ Metric.ball z R) : ‖φ x‖ ≤ ↑(iHolNNNorm φ z R t)

theorem norm_le_iHolNNNorm_of_subset {X : Type u_1} {𝕜 : Type u_2} {x z : X} {R t : ℝ} {φ : X → 𝕜} [MetricSpace X] [NormedField 𝕜] (hφ : iHolENorm φ z R t ≠ ⊤) (h : Function.support φ ⊆ Metric.ball z R) : ‖φ x‖ ≤ ↑(iHolNNNorm φ z R t)