OAI/Combinatorics/HadwigerCounterexample/LeafMixtures.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Leaf Mixtures

  1. structure OAI.HadwigerCounterexample.LeafMixture line 13
  2. abbrev OAI.HadwigerCounterexample.LeafMixture.X line 18
  3. instance OAI.HadwigerCounterexample.LeafMixture.(instance at line 20) line 20
  4. def OAI.HadwigerCounterexample.LeafMixture.poller line 22
  5. theorem OAI.HadwigerCounterexample.LeafMixture.poller_eq line 26
  6. def OAI.HadwigerCounterexample.LeafMixture.rooting line 32
  7. def OAI.HadwigerCounterexample.LeafMixture.amount line 33
  8. def OAI.HadwigerCounterexample.LeafMixture.sap line 34
  9. structure OAI.HadwigerCounterexample.LeafMixture.strength line 37
  10. theorem OAI.HadwigerCounterexample.LeafMixture.root_bound line 42
  11. theorem OAI.HadwigerCounterexample.LeafMixture.strength.slide line 50
  12. theorem OAI.HadwigerCounterexample.LeafMixture.sapLaw line 60
  13. def OAI.HadwigerCounterexample.LeafMixture.within line 62
  14. theorem OAI.HadwigerCounterexample.LeafMixture.in_parent line 63
  15. theorem OAI.HadwigerCounterexample.LeafMixture.present line 65
  16. theorem OAI.HadwigerCounterexample.LeafMixture.upper_sap line 67
  17. theorem OAI.HadwigerCounterexample.LeafMixture.upperSide line 70
  18. theorem OAI.HadwigerCounterexample.LeafMixture.grove_first line 79

    Source documentation

    first rural pack.

    theorem grove_first (ζ D : ℝ) (K : ℕ) (hz : 0<ζ) (hz' : ζ < 1)
    (hn : 0<N)
    (hR : ∀ a : Pin p n N, pr μ a.agree ≤ fee N (ζ/4) (planRank a.sp))
    (hc : ∀ x,w x ≤ bp (D*N)*μ x)
    (hw : ∀ x,0≤w x) (P : X p n N→Prop)
    (hK : D+ζ ≤ (ζ-ζ/4)*K) :
    ∃ s : LeafMixture p n N,s.strength w μ (D+K+1) ζ K ∧ s.within P ∧
      pr w P-bp (-ζ*N) ≤ s.amount w := by
…

    Mentions: OAI.HadwigerCounterexample.Pin, OAI.HadwigerCounterexample.pr, OAI.HadwigerCounterexample.fee, OAI.HadwigerCounterexample.planRank, OAI.HadwigerCounterexample.bp, OAI.HadwigerCounterexample.LeafMixture.X, OAI.HadwigerCounterexample.LeafMixture

  19. def OAI.HadwigerCounterexample.LeafMixture.elder line 105
  20. theorem OAI.HadwigerCounterexample.LeafMixture.ancestral line 108
  21. theorem OAI.HadwigerCounterexample.LeafMixture.elder_trim line 113
  22. theorem OAI.HadwigerCounterexample.LeafMixture.elder_weave line 132