OAI/Combinatorics/BinaryEdit/ScalarCutsBool.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Scalar finite cut decomposition used by the finite-group obstruction. This is the one-real-coordinate part of lem:cuts in preliminaries.tex.

  1. def OAI.TreeEdit.BinaryLower.BoolCuts.bit line 12
  2. def OAI.TreeEdit.BinaryLower.BoolCuts.cutDistance line 14
  3. lemma OAI.TreeEdit.BinaryLower.BoolCuts.cutDistance_nonneg line 17
  4. lemma OAI.TreeEdit.BinaryLower.BoolCuts.cutDistance_const line 20
  5. def OAI.TreeEdit.BinaryLower.BoolCuts.step line 24

    Source documentation

    A threshold viewed as a real-valued zero-one step.

    noncomputable def step (k i : ℕ) : ℝ := if k < i then 1 else 0
  6. lemma OAI.TreeEdit.BinaryLower.BoolCuts.step_mono line 26
  7. lemma OAI.TreeEdit.BinaryLower.BoolCuts.step_abs_sub line 35
  8. lemma OAI.TreeEdit.BinaryLower.BoolCuts.sum_gap_step line 40
  9. lemma OAI.TreeEdit.BinaryLower.BoolCuts.gap_cut_identity_of_le line 55
  10. lemma OAI.TreeEdit.BinaryLower.BoolCuts.gap_cut_identity line 64
  11. lemma OAI.TreeEdit.BinaryLower.BoolCuts.group_cuts line 74

    Source documentation

    Group an arbitrary finite collection of cuts by the Boolean function it defines. The two trivial cuts are discarded, since their distances vanish.

    lemma group_cuts {S I : Type*} [Fintype S] [DecidableEq S] [Fintype I]
    (C : I → S → Bool) (w : I → ℝ) (hw : ∀ i, 0 ≤ w i) :
    ∃ a : (S → Bool) → ℝ,
      (∀ D, 0 ≤ a D) ∧
      (∀ x y, ∑ i, w i * cutDistance (C i) x y =
        ∑ D, a D * cutDistance D x y) ∧
      a (fun _ => false) = 0 ∧ a (fun _ => true) = 0 := by
…

    Mentions: OAI.TreeEdit.BinaryLower.BoolCuts.cutDistance

  12. theorem OAI.TreeEdit.BinaryLower.BoolCuts.scalar_cut_representation line 116

    Source documentation

    Every real-valued function on a finite set is a nonnegative combination of cut metrics. The two constant cuts receive zero weight.

    theorem scalar_cut_representation {S : Type*} [Fintype S] [DecidableEq S]
    (f : S → ℝ) :
    ∃ a : (S → Bool) → ℝ,
      (∀ C, 0 ≤ a C) ∧
      (∀ x y, |f x - f y| = ∑ C, a C * cutDistance C x y) ∧
      a (fun _ => false) = 0 ∧ a (fun _ => true) = 0 := by
…

    Mentions: OAI.TreeEdit.BinaryLower.BoolCuts.cutDistance