OAI/Analysis/LipschitzHilbert/Estimates/MixedNorms.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite mixed-norm comparisons for the diagonal Hilbert-valued extension.

  1. theorem OAI.LipschitzHilbert.PhaseCombinatorics.finite_minkowski line 15
  2. theorem OAI.LipschitzHilbert.PhaseCombinatorics.mixed_norm_comparison line 34

    Source documentation

    Interchanging the finite ℓ^r and ℓ² norms costs no constant when r ≤ 2.

    theorem mixed_norm_comparison (x : ι → κ → ℝ) (hx : ∀ i j, 0 ≤ x i j)
    {r : ℝ} (hr : 0 < r) (hr2 : r ≤ 2) :
    (∑ j, (∑ i, x i j ^ r) ^ (2 / r)) ≤
      (∑ i, (∑ j, x i j ^ 2) ^ (r / 2)) ^ (2 / r) := by
…