OAI/Analysis/LipschitzHilbert/Estimates/FiniteVariation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LipschitzHilbert.finiteCubicVariation line 15
2. theorem OAI.LipschitzHilbert.finiteCubicVariation_nonneg line 22
3. theorem OAI.LipschitzHilbert.partition_le_finiteCubicVariation line 30
4. theorem OAI.LipschitzHilbert.scalar_finiteCubicVariation line 40
5. theorem OAI.LipschitzHilbert.euclidean_partition_variation_le line 74

   Source documentation

   Minkowski in ℓ^(3/2) moves the Euclidean coordinates outside the variation. The constant does not depend on the number of coordinates.

   theorem euclidean_partition_variation_le {κ : Type*} [Fintype κ]
       (F : ℕ → EuclideanSpace ℝ κ) (N : ℕ)
       (p : Fin (N + 1) → Fin (N + 1)) :
       (∑ i : Fin N, ‖F (p i.succ) - F (p i.castSucc)‖ ^ 3) ^ (2 / 3 : ℝ) ≤
         ∑ k, (∑ i : Fin N,
           ‖F (p i.succ) k - F (p i.castSucc) k‖ ^ 3) ^ (2 / 3 : ℝ) := by
   …

6. theorem OAI.LipschitzHilbert.euclidean_finiteCubicVariation_le line 97