OAI/Analysis/LpDimension/ExactDiscretization.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SubpolynomialLp.exact_discretization_all_lengths line 13

   Source documentation

   Exact finite discretization in n.choose 2 coordinates, including empty and singleton families.

   theorem exact_discretization_all_lengths (p : ℝ) (hp : 1 ≤ p) (n : ℕ)
       {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
       (x : Fin n → Lp ℝ (ENNReal.ofReal p) μ) (hx : Function.Injective x) :
       ∃ y : Fin n → Fin (n.choose 2) → ℝ, ∀ i j,
         coordinateDistance p (y i) (y j) = ‖x i - x j‖ := by
   …

   Mentions: OAI.SubpolynomialLp.coordinateDistance

2. theorem OAI.SubpolynomialLpExact.exact_discretization_embedding line 36

   Source documentation

   Every finite subset of a real Lp space embeds injectively into n.choose 2 real coordinates with their finite Lp distance.

   theorem exact_discretization_embedding (p : ℝ) (hp : 1 ≤ p) (n : ℕ)
       {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
       (x : Fin n → Lp ℝ (ENNReal.ofReal p) μ) (hx : Function.Injective x) :
       ∃ y : Fin n → Fin (n.choose 2) → ℝ, Function.Injective y ∧
         ∀ i j, coordinateDistance p (y i) (y j) = ‖x i - x j‖ := by
   …

3. theorem OAI.SubpolynomialLpExact.exact_discretization_lp_embedding line 57

   Source documentation

   The exact discretization is an injective embedding into the real Lp space on n.choose 2 points equipped with counting measure.

   theorem exact_discretization_lp_embedding (p : ℝ) (hp : 1 ≤ p) (n : ℕ)
       {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
       (x : Fin n → Lp ℝ (ENNReal.ofReal p) μ) (hx : Function.Injective x) :
       ∃ y : Fin n → Lp ℝ (ENNReal.ofReal p)
           (Measure.count : Measure (Fin (n.choose 2))),
         Function.Injective y ∧ ∀ i j, ‖y i - y j‖ = ‖x i - x j‖ := by
   …