Inhomogeneous Lipschitz norm

This file defines the Lipschitz 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.

TODO The iLipENorm should be properly generalized to Mathlib standards. Until then, it is defined in Defs.lean instead. See PR #493.

/-- The inhomogeneous Lipschitz norm on a ball. -/ def iLipENorm (φ : X → 𝕜) (x₀ : X) (R : ℝ) : ℝ≥0∞ := (⨆ x ∈ ball x₀ R, ‖φ x‖ₑ) + ENNReal.ofReal R * ⨆ (x ∈ ball x₀ R) (y ∈ ball x₀ R) (_ : x ≠ y), ‖φ x - φ y‖ₑ / edist x y

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

The NNReal version of the inhomogeneous Lipschitz norm on a ball, iLipENorm.

Equations

• iLipNNNorm φ x₀ R = (iLipENorm φ x₀ R).toNNReal

theorem iLipENorm_le_add {𝕜 : Type u_1} {X : Type u_2} {z : X} {R : ℝ} {C C' : NNReal} {φ : X → 𝕜} [MetricSpace X] [NormedField 𝕜] (h : ∀ x ∈ Metric.ball z R, ‖φ x‖ ≤ ↑C) (h' : ∀ x ∈ Metric.ball z R, ∀ x' ∈ Metric.ball z R, x ≠ x' → ‖φ x - φ x'‖ ≤ ↑C' * dist x x' / R) : iLipENorm φ z R ≤ ↑C + ↑C'

theorem iLipENorm_le {𝕜 : Type u_1} {X : Type u_2} {z : X} {R : ℝ} {C : NNReal} {φ : X → 𝕜} [MetricSpace X] [NormedField 𝕜] (h : ∀ x ∈ Metric.ball z R, ‖φ x‖ ≤ 2⁻¹ * ↑C) (h' : ∀ x ∈ Metric.ball z R, ∀ x' ∈ Metric.ball z R, x ≠ x' → ‖φ x - φ x'‖ ≤ 2⁻¹ * ↑C * dist x x' / R) : iLipENorm φ z R ≤ ↑C

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

theorem LipschitzOnWith.of_iLipENorm_ne_top {𝕜 : Type u_1} {X : Type u_2} {z : X} {R : ℝ} {φ : X → 𝕜} [MetricSpace X] [NormedField 𝕜] (hφ : iLipENorm φ z R ≠ ⊤) : LipschitzOnWith (iLipNNNorm φ z R / R.toNNReal) φ (Metric.ball z R)

theorem continuous_of_iLipENorm_ne_top {𝕜 : Type u_1} {X : Type u_2} [MetricSpace X] [NormedField 𝕜] {z : X} {R : ℝ} {φ : X → 𝕜} (hφ : tsupport φ ⊆ Metric.ball z R) (h'φ : iLipENorm φ z R ≠ ⊤) : Continuous φ

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

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