OAI/Analysis/LpDimension/Discretization.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SubpolynomialLp.PairIndex line 13
2. instance OAI.SubpolynomialLp.(instance at line 14) line 14
3. lemma OAI.SubpolynomialLp.pairIndex_card line 16
4. def OAI.SubpolynomialLp.pairPower line 22
5. lemma OAI.SubpolynomialLp.pairPower_nonneg line 25
6. lemma OAI.SubpolynomialLp.pairPower_continuous line 28
7. lemma OAI.SubpolynomialLp.pairPower_pair_le_sum line 35
8. lemma OAI.SubpolynomialLp.pairPower_sum_bound line 43
9. def OAI.SubpolynomialLp.normalizedLabels line 54
10. def OAI.SubpolynomialLp.normalizedPowers line 57
11. lemma OAI.SubpolynomialLp.normalizedLabels_compact line 60
12. lemma OAI.SubpolynomialLp.normalizedPowers_compact line 71
13. lemma OAI.SubpolynomialLp.normalizedPowers_sum line 75
14. lemma OAI.SubpolynomialLp.pairPower_smul_sub line 80
15. lemma OAI.SubpolynomialLp.pairPower_normalize line 87
16. lemma OAI.SubpolynomialLp.lp_norm_rpow_integral line 106
17. lemma OAI.SubpolynomialLp.lpDifference_integrable line 115
18. lemma OAI.SubpolynomialLp.lpDifference_integral line 123
19. lemma OAI.SubpolynomialLp.pad_coordinates line 133
20. lemma OAI.SubpolynomialLp.exact_discretization_ge_one line 146

    Source documentation

    Ball's finite-coordinate isometry, obtained by applying Carathéodory's theorem to the normalized pairwise pth powers.

    lemma exact_discretization_ge_one (p : ℝ) (hp : 1 ≤ p) (n : ℕ) (hn : 2 ≤ n)
        {Ω : Type uΩ} [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

21. lemma OAI.SubpolynomialLp.exact_discretization line 224