OAI/Combinatorics/PlanarL1/FiniteL1.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarL1.FiniteL1.ofFunction line 14
  2. lemma OAI.PlanarL1.FiniteL1.norm_ofFunction line 17
  3. lemma OAI.PlanarL1.FiniteL1.ofFunction_sub line 27
  4. lemma OAI.PlanarL1.FiniteL1.norm_sub line 32
  5. def OAI.PlanarL1.FiniteL1.cutMap line 37

    Source documentation

    The final finite cut-coordinate formula, valued in the ACTUAL real L1 space requested by the main theorem, rather than an abstract cut cone.

    noncomputable def cutMap {V : Type*} (cut : I → Set V) (weight : I → ℝ) (v : V) :
    Lp ℝ 1 (Measure.count : Measure I) := by
…
  6. lemma OAI.PlanarL1.FiniteL1.norm_cutMap line 42
  7. structure OAI.PlanarL1.FiniteL1.BinarySystem line 70

    Source documentation

    Binary measurable assignments with integrable pair differences; individual sets may have infinite measure, exactly as for the paper's label half-lines.

    structure BinarySystem where
…
  8. def OAI.PlanarL1.FiniteL1.BinarySystem.indicator line 79
  9. def OAI.PlanarL1.FiniteL1.BinarySystem.fiber line 80
  10. def OAI.PlanarL1.FiniteL1.BinarySystem.fiberValue line 81
  11. def OAI.PlanarL1.FiniteL1.BinarySystem.Proper line 83
  12. def OAI.PlanarL1.FiniteL1.BinarySystem.contribution line 85
  13. def OAI.PlanarL1.FiniteL1.BinarySystem.weight line 88
  14. lemma OAI.PlanarL1.FiniteL1.BinarySystem.measurable_fiber line 90
  15. lemma OAI.PlanarL1.FiniteL1.BinarySystem.measurable_fiberValue line 99
  16. lemma OAI.PlanarL1.FiniteL1.BinarySystem.measurable_contribution line 102
  17. lemma OAI.PlanarL1.FiniteL1.BinarySystem.contribution_nonneg line 109
  18. lemma OAI.PlanarL1.FiniteL1.BinarySystem.integrable_contribution line 113
  19. lemma OAI.PlanarL1.FiniteL1.BinarySystem.weight_nonneg line 135
  20. def OAI.PlanarL1.FiniteL1.BinarySystem.cutCost line 138
  21. lemma OAI.PlanarL1.FiniteL1.BinarySystem.cutCost_nonneg line 142
  22. lemma OAI.PlanarL1.FiniteL1.BinarySystem.cutCost_eq_zero_of_not_proper line 145
  23. lemma OAI.PlanarL1.FiniteL1.BinarySystem.sum_contribution line 154
  24. lemma OAI.PlanarL1.FiniteL1.BinarySystem.cut_decomposition line 178

    Source documentation

    Exact cut coefficients, not a finite-dimensional approximation of the label metric. Empty/full cuts are zero; proper weights are finite by pair integrability.

    lemma cut_decomposition (x y : V) :
    ∑ S : Set V, B.weight S * cutCost S x y =
      ∫ ω, |B.indicator x ω-B.indicator y ω| ∂μ := by
…

    Mentions: OAI.PlanarL1.FiniteL1.BinarySystem.cutCost

  25. def OAI.PlanarL1.FiniteL1.BinarySystem.embedding line 195
  26. lemma OAI.PlanarL1.FiniteL1.BinarySystem.distance_embedding line 198
  27. structure OAI.PlanarL1.FiniteL1.CutFamily line 216

    Source documentation

    All final metrics, and all adaptive averages of them, use the same finite cut index type. No finite approximation to the label space is made.

    structure CutFamily (V : Type*) where
…
  28. def OAI.PlanarL1.FiniteL1.CutFamily.distance line 223
  29. lemma OAI.PlanarL1.FiniteL1.CutFamily.distance_nonneg line 227
  30. def OAI.PlanarL1.FiniteL1.CutFamily.ofBinary line 231
  31. lemma OAI.PlanarL1.FiniteL1.CutFamily.distance_ofBinary line 234
  32. def OAI.PlanarL1.FiniteL1.CutFamily.add line 239
  33. lemma OAI.PlanarL1.FiniteL1.CutFamily.distance_add line 243
  34. def OAI.PlanarL1.FiniteL1.CutFamily.sum line 248
  35. lemma OAI.PlanarL1.FiniteL1.CutFamily.distance_sum line 252
  36. def OAI.PlanarL1.FiniteL1.CutFamily.average line 258
  37. lemma OAI.PlanarL1.FiniteL1.CutFamily.distance_average line 262
  38. def OAI.PlanarL1.FiniteL1.CutFamily.scale line 273
  39. lemma OAI.PlanarL1.FiniteL1.CutFamily.distance_scale line 277
  40. def OAI.PlanarL1.FiniteL1.CutFamily.embedding line 284
  41. lemma OAI.PlanarL1.FiniteL1.CutFamily.norm_embedding line 287
  42. theorem OAI.PlanarL1.FiniteL1.CutFamily.embedding_of_bounds line 294

    Source documentation

    The last rescaling step in the manuscript, using actual real Lp1. The geometric lower bound is a prerequisite proved by the random construction.

    theorem embedding_of_bounds (C : CutFamily V) (d : V → V → ℝ) {a b : ℝ}
    (ha : 0 < a) (hl : ∀ x y, a*d x y ≤ C.distance x y)
    (hu : ∀ x y, C.distance x y ≤ b*d x y) :
    ∃ f : V → Lp ℝ 1 (Measure.count : Measure (Set V)),
      ∀ x y, d x y ≤ ‖f x-f y‖ ∧ ‖f x-f y‖ ≤ (b/a)*d x y := by
…

    Mentions: OAI.PlanarL1.FiniteL1.CutFamily