OAI/Geometry/PinnedDistances/TreeTransport.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPinned.Cuts.Laminar line 43
2. def OAI.WeakPinned.Cuts.value line 46
3. def OAI.WeakPinned.Cuts.mass line 49
4. lemma OAI.WeakPinned.Cuts.laminar_erase line 52
5. lemma OAI.WeakPinned.Cuts.minimal_constant line 56
6. lemma OAI.WeakPinned.Cuts.value_erase line 77
7. lemma OAI.WeakPinned.Cuts.signed_lipschitz_bound line 86

   Source documentation

   Dual tree transport with completely explicit cut cost. The signed measure b has total mass zero. Neither nonnegativity nor coupling existence is needed.

   lemma signed_lipschitz_bound (s : Finset (Finset P)) (hs : Laminar s)
       (b : P → ℝ) (hb : ∑ x, b x=0) (d : Finset P → ℝ) (a : ℝ)
       (g : ℝ → ℝ) (hg : ∀ u v, |g u-g v| ≤ |u-v|) :
       |∑ x, b x*g (value s d a x)| ≤ ∑ C ∈ s, |d C| * |mass b C| := by
   …

   Mentions: OAI.WeakPinned.Cuts.Laminar, OAI.WeakPinned.Cuts.value, OAI.WeakPinned.Cuts.mass

8. def OAI.WeakPinned.Cuts.ind line 125
9. def OAI.WeakPinned.Cuts.distance line 127
10. def OAI.WeakPinned.Cuts.rootDistance line 130
11. def OAI.WeakPinned.Cuts.coeff line 133
12. def OAI.WeakPinned.Cuts.cost line 136
13. lemma OAI.WeakPinned.Cuts.distance_symm line 140
14. lemma OAI.WeakPinned.Cuts.distance_nonneg line 145
15. lemma OAI.WeakPinned.Cuts.distance_as_value line 150
16. lemma OAI.WeakPinned.Cuts.abs_coeff line 158
17. lemma OAI.WeakPinned.Cuts.function_transfer line 163
18. lemma OAI.WeakPinned.Cuts.first_fluctuation_transfer line 175
19. lemma OAI.WeakPinned.Cuts.value_sub line 185
20. lemma OAI.WeakPinned.Cuts.last_fluctuation_transfer line 195
21. lemma OAI.WeakPinned.Cuts.mass_nonneg line 220
22. lemma OAI.WeakPinned.Cuts.expected_cut line 223
23. lemma OAI.WeakPinned.Cuts.expected_distance_ge line 236
24. lemma OAI.WeakPinned.Cuts.exists_zero_cell line 257
25. lemma OAI.WeakPinned.Cuts.fluctuation_lower line 283

    Source documentation

    A minimal positive cut collapses a set of mass at least η to a single pseudometric point. This gives a direct fluctuation bound without constructing a tree graph.

    lemma fluctuation_lower (s : Finset (Finset P)) (hs : Laminar s)
        (l : Finset P → ℝ) (hl : ∀ C ∈ s, 0 ≤ l C) (p : P → ℝ)
        (hp0 : ∀ x, 0 ≤ p x) (hp : ∑ x, p x=1) (η : ℝ) (hη : 0 ≤ η)
        (hbal : ∀ C ∈ s, 0 < l C → η ≤ mass p C ∧ η ≤ 1-mass p C) :
        η^3*(∑ C ∈ s, l C) ≤
          ∑ y, p y*∑ x', p x'*∑ x, p x*|distance s l x y-distance s l x' y| := by
    …

    Mentions: OAI.WeakPinned.Cuts.Laminar, OAI.WeakPinned.Cuts.mass, OAI.WeakPinned.Cuts.distance

26. lemma OAI.WeakPinned.Cuts.cost_symm line 330
27. def OAI.WeakPinned.Cuts.fluctuation line 333
28. def OAI.WeakPinned.Cuts.doubleMean line 336
29. lemma OAI.WeakPinned.Cuts.fluctuation_symm line 340
30. lemma OAI.WeakPinned.Cuts.sum_le_add_of_abs line 343
31. lemma OAI.WeakPinned.Cuts.doubleMean_transfer line 346
32. lemma OAI.WeakPinned.Cuts.doubleMean_fiber line 375
33. lemma OAI.WeakPinned.Cuts.last_doubleMean_transfer line 391
34. lemma OAI.WeakPinned.Cuts.iid_transfer line 420

    Source documentation

    Finite transport to independent sampling with explicit cut costs.

    lemma iid_transfer (s : Finset (Finset P)) (hs : Laminar s)
        (l : Finset P → ℝ) (hl : ∀ C ∈ s, 0 ≤ l C) (a t : P → ℝ) (ρ : P → P → ℝ)
        (ha0 : ∀ x, 0 ≤ a x) (ht0 : ∀ y, 0 ≤ t y) (hρ0 : ∀ y x, 0 ≤ ρ y x)
        (ha : ∑ x, a x=1) (ht : ∑ y, t y=1) (hρ : ∀ y, ∑ x, ρ y x=1) (R : P → ℝ) :
        (∑ y, a y*doubleMean s l a y) ≤
          2*(∑ y, t y*∑ x, ρ y x*|distance s l x y-R y|)+
          2*(∑ y, t y*cost s l (ρ y) a)+2*cost s l t a := by
    …

    Mentions: OAI.WeakPinned.Cuts.Laminar, OAI.WeakPinned.Cuts.doubleMean, OAI.WeakPinned.Cuts.distance, OAI.WeakPinned.Cuts.cost