OAI/Combinatorics/BinaryEdit/CutAggregation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TreeEdit.BinaryLower.CutAggregation.summable_L1_abs_sub line 15
2. lemma OAI.TreeEdit.BinaryLower.CutAggregation.norm_L1_sub line 20
3. lemma OAI.TreeEdit.BinaryLower.CutAggregation.scalar_weight_le line 28

   Source documentation

   A nontrivial cut weight is dominated by any coordinate distance across that cut. This makes the countable grouping legitimate without a finite support assumption on the image in ℓ₁.

   lemma scalar_weight_le {S : Type u} {C : Type v} [Fintype C]
       (f : S → ℝ) (U : C → S → ℝ) (a : C → ℝ)
       (ha : ∀ c, 0 ≤ a c)
       (hrep : ∀ x y, |f x - f y| = ∑ c, a c * |U c x - U c y|)
       (c : C) (x y : S) (hxy : |U c x - U c y| = 1) :
       a c ≤ |f x - f y| := by
   …

4. theorem OAI.TreeEdit.BinaryLower.CutAggregation.aggregate line 45

   Source documentation

   Countably many scalar decompositions combine into an actual finite cut representation of a map into the full absolutely summable sequence space. Null cuts are permitted, but their coordinate weights must vanish.

   theorem aggregate {S : Type u} {C : Type v} [Fintype C]
       (F : S → TreeEdit.RealL1) (U : C → S → ℝ) (a : ℕ → C → ℝ)
       (ha : ∀ n c, 0 ≤ a n c)
       (hcut : ∀ c, (∀ n, a n c = 0) ∨ ∃ x y, |U c x - U c y| = 1)
       (hrep : ∀ n x y,
         |F x n - F y n| = ∑ c, a n c * |U c x - U c y|) :
       ∃ A : C → ℝ, (∀ c, 0 ≤ A c) ∧
         (∀ c, A c = ∑' n, a n c) ∧
         (∀ x y, ‖F x - F y‖ = ∑ c, A c * |U c x - U c y|) := by
   …

   Mentions: OAI.TreeEdit.RealL1

5. theorem OAI.TreeEdit.BinaryLower.CutAggregation.cut_mass_bound line 78

   Source documentation

   Every nontrivial cut separates two ordered pairs. Hence the finite total cut mass is bounded by the sum over unordered pairs, written as one half of the ordered-pair sum (diagonal terms vanish automatically).

   theorem cut_mass_bound {S : Type u} {C : Type v} [Fintype S] [Fintype C]
       (F : S → TreeEdit.RealL1) (U : C → S → ℝ) (A : C → ℝ)
       (hA : ∀ c, 0 ≤ A c)
       (hcut : ∀ c, A c = 0 ∨ ∃ x y, |U c x - U c y| = 1)
       (hrep : ∀ x y, ‖F x - F y‖ = ∑ c, A c * |U c x - U c y|) :
       ∑ c, A c ≤ (∑ p : S × S, ‖F p.1 - F p.2‖) / 2 := by
   …

   Mentions: OAI.TreeEdit.RealL1

6. theorem OAI.TreeEdit.BinaryLower.CutAggregation.aggregate_with_mass_bound line 118

   Source documentation

   Countable scalar decompositions yield a finite cut representation with bounded total weight.

   theorem aggregate_with_mass_bound {S : Type u} {C : Type v}
       [Fintype S] [Fintype C]
       (F : S → TreeEdit.RealL1) (U : C → S → ℝ) (a : ℕ → C → ℝ)
       (ha : ∀ n c, 0 ≤ a n c)
       (hcut : ∀ c, (∀ n, a n c = 0) ∨ ∃ x y, |U c x - U c y| = 1)
       (hrep : ∀ n x y,
         |F x n - F y n| = ∑ c, a n c * |U c x - U c y|) :
       ∃ A : C → ℝ, (∀ c, 0 ≤ A c) ∧
         (∀ c, A c = ∑' n, a n c) ∧
         (∀ x y, ‖F x - F y‖ = ∑ c, A c * |U c x - U c y|) ∧
         (∑ c, A c ≤ (∑ p : S × S, ‖F p.1 - F p.2‖) / 2) := by
   …

   Mentions: OAI.TreeEdit.RealL1