OAI/Combinatorics/HadwigerCounterexample/WeightedPartitions.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Weighted Partitions

  1. abbrev OAI.HadwigerCounterexample.Tiles line 13
  2. def OAI.HadwigerCounterexample.inTiles line 14
  3. def OAI.HadwigerCounterexample.apart line 16
  4. def OAI.HadwigerCounterexample.partMass line 19
  5. def OAI.HadwigerCounterexample.partW line 20
  6. def OAI.HadwigerCounterexample.allMass line 22
  7. def OAI.HadwigerCounterexample.allW line 23
  8. theorem OAI.HadwigerCounterexample.issued_sub line 27
  9. theorem OAI.HadwigerCounterexample.issued_law line 33
  10. theorem OAI.HadwigerCounterexample.ind_tiles line 43
  11. theorem OAI.HadwigerCounterexample.tiles_inter line 56
  12. theorem OAI.HadwigerCounterexample.mass_apart line 61
  13. def OAI.HadwigerCounterexample.portionW line 64
  14. theorem OAI.HadwigerCounterexample.rebuild line 67
  15. theorem OAI.HadwigerCounterexample.improve line 92

    Source documentation

    Refine on every old tile, with rules allowed to be different on every tile. Total loss bound relative to the old tiled union.

    theorem improve (T : Tiles A) (w : Wgt A) (hw : ∀ x,0 ≤ w x)
    (P : A→Prop) (R : Finset A→Finset A→Prop) (hT : apart T) {c : ℝ}
    (h : ∀ i∈T,∃ V : Tiles A, apart V ∧
      (∀ S∈V,S ⊆ i ∧ R i S) ∧
      pr (partW w i) (fun x => x∈i∧P x∧¬inTiles V x) ≤ c) :
    ∃ V : Tiles A,apart V∧ (∀ S∈V,∃ i∈T,S⊆i ∧ R i S) ∧
      pr w (fun x => inTiles T x ∧ P x ∧ ¬inTiles V x)≤ allMass w T*c := by
…

    Mentions: OAI.HadwigerCounterexample.Tiles, OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.apart, OAI.HadwigerCounterexample.pr, OAI.HadwigerCounterexample.partW, OAI.HadwigerCounterexample.inTiles, OAI.HadwigerCounterexample.allMass