OAI/Combinatorics/TreewidthL1/AnchorExperiment.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoundedTreewidthL1.AnchorExperiment.count line 12
  2. instance OAI.BoundedTreewidthL1.AnchorExperiment.count_neZero line 13
  3. def OAI.BoundedTreewidthL1.AnchorExperiment.particleLip line 14
  4. def OAI.BoundedTreewidthL1.AnchorExperiment.upper line 15
  5. lemma OAI.BoundedTreewidthL1.AnchorExperiment.count_ge line 16
  6. lemma OAI.BoundedTreewidthL1.AnchorExperiment.particleLip_pos line 17
  7. lemma OAI.BoundedTreewidthL1.AnchorExperiment.upper_pos line 20
  8. abbrev OAI.BoundedTreewidthL1.AnchorExperiment.Space line 30
  9. def OAI.BoundedTreewidthL1.AnchorExperiment.measure line 31
  10. instance OAI.BoundedTreewidthL1.AnchorExperiment.probability line 32
  11. def OAI.BoundedTreewidthL1.AnchorExperiment.noise line 36
  12. def OAI.BoundedTreewidthL1.AnchorExperiment.states line 37
  13. def OAI.BoundedTreewidthL1.AnchorExperiment.raw line 39
  14. structure OAI.BoundedTreewidthL1.AnchorExperiment.Model line 44
  15. def OAI.BoundedTreewidthL1.AnchorExperiment.Model.datum line 76
  16. lemma OAI.BoundedTreewidthL1.AnchorExperiment.Model.datum_dist line 79
  17. lemma OAI.BoundedTreewidthL1.AnchorExperiment.Model.M_pos line 81
  18. lemma OAI.BoundedTreewidthL1.AnchorExperiment.Model.height line 84
  19. lemma OAI.BoundedTreewidthL1.AnchorExperiment.Model.lipschitz line 88
  20. lemma OAI.BoundedTreewidthL1.AnchorExperiment.Model.pair_distinct line 92
  21. lemma OAI.BoundedTreewidthL1.AnchorExperiment.Model.gap_probability line 100
  22. lemma OAI.BoundedTreewidthL1.AnchorExperiment.Model.height_test line 122
  23. lemma OAI.BoundedTreewidthL1.AnchorExperiment.Model.launch_test line 180
  24. theorem OAI.BoundedTreewidthL1.AnchorExperiment.model_exists line 226

    Source documentation

    Every chosen actual finite ordinary seed produces the ensemble; no consistency or global lower comparison is an assumption.

    theorem model_exists {V : Type*} [Fintype V] [DecidableEq V] {n : ℕ}
    (G : SimpleGraph V) (hG : G.Connected) (ℓ : G.edgeSet → ℝ) (hℓ : ∀ e, 0 < ℓ e)
    (T : SimpleGraph (Fin (n+1))) (hT : T.IsTree) (root : Fin (n+1))
    (B : Fin (n+1) → Finset V) (hne : ∀ i, (B i).Nonempty)
    (hcover : ∀ v, ∃ i, v ∈ B i)
    (hedge : ∀ u v, G.Adj u v → ∃ i, u ∈ B i ∧ v ∈ B i)
    (hrun : ∀ v, (T.induce {i | v ∈ B i}).Connected)
    (k : ℕ) (hbag : ∀ i, (B i).card ≤ k) (J α π η : ℝ) :
    let := weightedMetricSpace G ℓ hG hℓ
…

    Mentions: OAI.BoundedTreewidthL1.weightedMetricSpace