OAI/Combinatorics/TreewidthL1/Cuts.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoundedTreewidthL1.thresholdLabels line 13
  2. def OAI.BoundedTreewidthL1.sweep line 16
  3. def OAI.BoundedTreewidthL1.complementCut line 19
  4. def OAI.BoundedTreewidthL1.symmetrizeCut line 21
  5. def OAI.BoundedTreewidthL1.cutEvent line 24
  6. def OAI.BoundedTreewidthL1.cutUncertainty line 27
  7. lemma OAI.BoundedTreewidthL1.measurable_thresholdLabels line 38
  8. instance OAI.BoundedTreewidthL1.sweep_finite line 50
  9. lemma OAI.BoundedTreewidthL1.cutEvent_measurable line 54
  10. lemma OAI.BoundedTreewidthL1.measurable_complementCut line 57
  11. instance OAI.BoundedTreewidthL1.symmetrizeCut_finite line 60
  12. lemma OAI.BoundedTreewidthL1.complementCut_involutive line 66
  13. def OAI.BoundedTreewidthL1.complementEquiv line 72
  14. lemma OAI.BoundedTreewidthL1.complement_preimage_event line 78
  15. lemma OAI.BoundedTreewidthL1.uncertainty_nonneg line 101
  16. lemma OAI.BoundedTreewidthL1.uncertainty_add line 107
  17. lemma OAI.BoundedTreewidthL1.uncertainty_complement line 120
  18. lemma OAI.BoundedTreewidthL1.uncertainty_symmetrize line 131
  19. lemma OAI.BoundedTreewidthL1.sweep_event line 148
  20. lemma OAI.BoundedTreewidthL1.thresholdLabels_constant_gap line 162
  21. lemma OAI.BoundedTreewidthL1.sweep_height_gap_unsymmetrized line 176
  22. theorem OAI.BoundedTreewidthL1.sweep_height_gap line 216
  23. lemma OAI.BoundedTreewidthL1.symmetrizeCut_add line 230
  24. lemma OAI.BoundedTreewidthL1.sweep_pair_gap_ordered line 235
  25. theorem OAI.BoundedTreewidthL1.sweep_launch_gap line 298
  26. def OAI.BoundedTreewidthL1.cutTrace line 335
  27. def OAI.BoundedTreewidthL1.cutSeparation line 338
  28. def OAI.BoundedTreewidthL1.CommonWeakOrder line 341
  29. def OAI.BoundedTreewidthL1.partialCutEvent line 345
  30. lemma OAI.BoundedTreewidthL1.cutMeasure_ext_all_true line 350

    Source documentation

    On a finite Boolean cube, all-true conjunctions determine a finite measure. The proof retains the total mass (the conjunction over the empty set).

    lemma cutMeasure_ext_all_true (μ ν : Measure (V → Bool)) [IsFiniteMeasure μ]
    [IsFiniteMeasure ν]
    (heq : ∀ P : Finset V, μ.real {ω | ∀ p ∈ P, ω p = true} =
      ν.real {ω | ∀ p ∈ P, ω p = true}) : μ = ν := by
…
  31. lemma OAI.BoundedTreewidthL1.sweep_all_true_of_min line 404
  32. lemma OAI.BoundedTreewidthL1.sweep_total_mass line 424
  33. lemma OAI.BoundedTreewidthL1.sweep_affine_of_common_min line 438
  34. lemma OAI.BoundedTreewidthL1.cutTrace_add line 465
  35. lemma OAI.BoundedTreewidthL1.cutTrace_sweep line 469
  36. theorem OAI.BoundedTreewidthL1.sweep_trace_update line 474
  37. lemma OAI.BoundedTreewidthL1.sweep_separation_ordered line 503
  38. theorem OAI.BoundedTreewidthL1.sweep_separation line 526