OAI/Combinatorics/Graphs/Coverage.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoordinateSweeps.Coverage.cutEdges line 16

   Source comment

   Oriented edges crossing a two-color cut.

   def cutEdges (R : I → I → Prop) (c : I → Bool) : Finset (I × I) :=
   …

   Mentions: OAI.CoordinateSweeps.c

2. theorem OAI.CoordinateSweeps.Coverage.mem_cutEdges line 20
3. theorem OAI.CoordinateSweeps.Coverage.exists_crossing_cut line 25

   Source comment

   A maximum cut has an opposite-color neighbor at every nonisolated vertex. Only symmetry and absence of loops are used.

   theorem exists_crossing_cut (R : I → I → Prop)
       (hsym : ∀ ⦃left right⦄, R left right → R right left) (hirr : ∀ vertex, ¬ R vertex vertex) :
       ∃ c : I → Bool, ∀ i, (∃ j, R i j) → ∃ j, R i j ∧ c i ≠ c j := by
   …

   Mentions: OAI.CoordinateSweeps.c

4. def OAI.CoordinateSweeps.Coverage.covered line 65

   Source comment

   Particles incident to a particle-sharing edge or a fixed hole.

   def covered (R : I → I → Prop) (T : I → H → Prop) : Finset I :=
   …

5. theorem OAI.CoordinateSweeps.Coverage.mem_covered line 69
6. theorem OAI.CoordinateSweeps.Coverage.exists_star_forest line 74

   Source comment

   A star forest supplies at least half as many distinct particle tails as there are covered particles, with all parents outside the chosen tails.

   theorem exists_star_forest (R : I → I → Prop) (T : I → H → Prop)
       (hsym : ∀ ⦃left right⦄, R left right → R right left) (hirr : ∀ vertex, ¬ R vertex vertex) :
       ∃ A : Finset I, A ⊆ covered R T ∧ (covered R T).card ≤ 2*A.card ∧
         ∀ i ∈ A, (∃ j, j ∉ A ∧ R i j) ∨ (∃ l, T i l) := by
   …

   Mentions: OAI.CoordinateSweeps.Coverage.covered

7. def OAI.CoordinateSweeps.Coverage.productMass line 122

   Source comment

   Product mass of independent particle data.

   def productMass (w : X → ℝ) (x : I → X) : ℝ := ∏ i, w (x i)

8. def OAI.CoordinateSweeps.Coverage.probability line 125

   Source comment

   Finite event probability, with the product law on the full endpoint array.

   def probability (w : X → ℝ) (P : (I → X) → Prop) : ℝ :=
   …

9. def OAI.CoordinateSweeps.Coverage.glue line 128
10. theorem OAI.CoordinateSweeps.Coverage.glue_mem line 132
11. theorem OAI.CoordinateSweeps.Coverage.glue_not_mem line 137
12. theorem OAI.CoordinateSweeps.Coverage.productMass_glue line 142
13. theorem OAI.CoordinateSweeps.Coverage.sum_prod_ite_all line 151

    Source comment

    Reused elementary finite independence identity, inline.

    theorem sum_prod_ite_all {J : Type*} [Fintype J] [DecidableEq J]
        {Y : J → Type*} [∀ j, Fintype (Y j)]
        (w : ∀ j, Y j → ℝ) (P : ∀ j, Y j → Prop) :
        (∑ x : ∀ j, Y j, if ∀ j, P j (x j) then ∏ j, w j (x j) else 0) =
          ∏ j, ∑ y, if P j y then w j y else 0 := by
    …

14. theorem OAI.CoordinateSweeps.Coverage.probability_star_factorization line 169

    Source comment

    Conditional on all roots, different star tails involve independent data. This is a factorization of the actual finite sum, not an independence axiom.

    theorem probability_star_factorization (A : Finset I) (w : X → ℝ)
        (P : ({i : I // i ∉ A} → X) → A → X → Prop) :
        probability w (fun x : I → X => ∀ i : A, P (fun j => x j) i (x i)) =
          ∑ y : {i : I // i ∉ A} → X,
            (∏ j, w (y j)) * ∏ i : A, ∑ t : X, if P y i t then w t else 0 := by
    …

    Mentions: OAI.CoordinateSweeps.Coverage.probability

15. theorem OAI.CoordinateSweeps.Coverage.probability_star_le line 202

    Source comment

    The source's leaf elimination bound for the star witnesses selected above.

    theorem probability_star_le (A : Finset I) (w : X → ℝ)
        (hw : ∀ x, 0 ≤ w x) (hs : ∑ x, w x = 1) (ω : ℝ) (hω : 0 ≤ ω)
        (P : ({i : I // i ∉ A} → X) → A → X → Prop)
        (hP : ∀ y i, (∑ t : X, if P y i t then w t else 0) ≤ ω) :
        probability w (fun x : I → X => ∀ i : A, P (fun j => x j) i (x i)) ≤ ω^A.card := by
    …

    Mentions: OAI.CoordinateSweeps.Coverage.probability

16. def OAI.CoordinateSweeps.Coverage.starSystem line 236

    Source comment

    A finite directed star system. Distinct tails are indexed by the subtype A; the parent lies outside A or is a hole.

    def starSystem (R : I → I → Prop) (T : I → H → Prop)
        (A : Finset I) (p : A → I ⊕ H) : Prop :=
    …

17. theorem OAI.CoordinateSweeps.Coverage.exists_star_system line 244

    Source comment

    The witness can be trimmed to any requested number of tails up to half (rounded up) of the number of covered particles.

    theorem exists_star_system (R : I → I → Prop) (T : I → H → Prop)
        (hsym : ∀ ⦃left right⦄, R left right → R right left) (hirr : ∀ vertex, ¬ R vertex vertex) (j : ℕ)
        (hj : j ≤ ((covered R T).card + 1)/2) :
        ∃ A : Finset I, A.card = j ∧ ∃ p : A → I ⊕ H, starSystem R T A p := by
    …

    Mentions: OAI.CoordinateSweeps.Coverage.covered, OAI.CoordinateSweeps.Coverage.starSystem

18. def OAI.CoordinateSweeps.Coverage.starEvent line 265

    Source comment

    The sharing event of one directed system under the full independent data. Forbidden parent choices simply give an empty event.

    def starEvent (S : X → X → Prop) (holes : H → X)
        (A : Finset I) (p : A → I ⊕ H) (x : I → X) : Prop :=
    …

19. def OAI.CoordinateSweeps.Coverage.rootPredicate line 270

    Source comment

    A tail predicate with the values at all its possible roots fixed.

    def rootPredicate (S : X → X → Prop) (holes : H → X)
        (A : Finset I) (p : A → I ⊕ H)
        (y : {i : I // i ∉ A} → X) (i : A) (t : X) : Prop :=
    …

20. theorem OAI.CoordinateSweeps.Coverage.starEvent_iff_root line 278
21. theorem OAI.CoordinateSweeps.Coverage.probability_starEvent_le line 291

    Source comment

    For every particular system of j distinct tails toward non-tail parents, the sharing probability is at most ω^j, with no layer independence premise.

    theorem probability_starEvent_le (S : X → X → Prop) (holes : H → X)
        (A : Finset I) (p : A → I ⊕ H) (w : X → ℝ)
        (hw : ∀ x, 0 ≤ w x) (hs : ∑ x, w x = 1) (ω : ℝ) (hω : 0 ≤ ω)
        (hS : ∀ y, (∑ t : X, if S t y then w t else 0) ≤ ω) :
        probability w (starEvent S holes A p) ≤ ω^A.card := by
    …

    Mentions: OAI.CoordinateSweeps.Coverage.probability, OAI.CoordinateSweeps.Coverage.starEvent

22. theorem OAI.CoordinateSweeps.Coverage.productMass_nonneg line 317
23. theorem OAI.CoordinateSweeps.Coverage.probability_mono line 320
24. theorem OAI.CoordinateSweeps.Coverage.probability_exists_le line 333
25. abbrev OAI.CoordinateSweeps.Coverage.Witness line 357

    Source comment

    Data encoding exactly j distinct tails and one arbitrary parent per tail. The sub-event enforces the star/root restrictions.

    abbrev Witness (I H : Type*) [Fintype I] (j : ℕ) :=
    …

26. theorem OAI.CoordinateSweeps.Coverage.card_witness_le line 360
27. def OAI.CoordinateSweeps.Coverage.sharingCoverage line 380

    Source comment

    Covered particles for the actual symmetric sharing relation on path data.

    def sharingCoverage (S : X → X → Prop) (holes : H → X) (x : I → X) : Finset I :=
    …

28. theorem OAI.CoordinateSweeps.Coverage.sharingCoverage_witness line 384
29. theorem OAI.CoordinateSweeps.Coverage.probability_coverage_le_nat line 407

    Source comment

    Source coverage bound with the slightly stronger integer exponent ceil(n/2). There is no independence assumption between different path layers.

    theorem probability_coverage_le_nat (S : X → X → Prop)
        (hSsym : ∀ ⦃left right⦄, S left right → S right left)
        (holes : H → X) (w : X → ℝ) (hw : ∀ x, 0 ≤ w x) (hs : ∑ x, w x = 1)
        (ω : ℝ) (hω : 0 ≤ ω)
        (hS : ∀ y, (∑ t : X, if S t y then w t else 0) ≤ ω) (n : ℕ) :
        probability w (fun x : I → X => n ≤ (sharingCoverage S holes x).card) ≤
          (2 : ℝ)^Fintype.card I *
            (((Fintype.card I + Fintype.card H : ℕ) : ℝ) * ω)^((n+1)/2) := by
    …

    Mentions: OAI.CoordinateSweeps.Coverage.probability, OAI.CoordinateSweeps.Coverage.sharingCoverage

30. theorem OAI.CoordinateSweeps.Coverage.probability_coverage_le line 441

    Source comment

    The literal source's coverage estimate (04:eq9), including zero sharing rate and zero requested coverage, with the real exponent n/2.

    theorem probability_coverage_le (S : X → X → Prop)
        (hSsym : ∀ ⦃left right⦄, S left right → S right left)
        (holes : H → X) (w : X → ℝ) (hw : ∀ x, 0 ≤ w x) (hs : ∑ x, w x = 1)
        (ω : ℝ) (hω : 0 ≤ ω)
        (hS : ∀ y, (∑ t : X, if S t y then w t else 0) ≤ ω)
        (hsmall : ((Fintype.card I + Fintype.card H : ℕ) : ℝ) * ω ≤ 1) (n : ℕ) :
        probability w (fun x : I → X => n ≤ (sharingCoverage S holes x).card) ≤
          (2 : ℝ)^Fintype.card I *
            ((((Fintype.card I + Fintype.card H : ℕ) : ℝ) * ω) ^ ((n : ℝ)/2)) := by
    …

    Mentions: OAI.CoordinateSweeps.Coverage.probability, OAI.CoordinateSweeps.Coverage.sharingCoverage

31. theorem OAI.CoordinateSweeps.Coverage.probability_many_hits_le line 482

    Source comment

    Independent occupancy of a fixed measurable subset. The set is fixed BEFORE taking probability, exactly as required in source04:eq12.

    theorem probability_many_hits_le (w : X → ℝ) (hw : ∀ x, 0 ≤ w x)
        (hs : ∑ x, w x = 1) (P : X → Prop) (p : ℝ) (hp : 0 ≤ p)
        (hP : (∑ x, if P x then w x else 0) ≤ p) (n : ℕ) :
        probability w (fun x : I → X => n ≤ (Finset.univ.filter (fun i => P (x i))).card) ≤
          (2 : ℝ)^Fintype.card I * p^n := by
    …

    Mentions: OAI.CoordinateSweeps.Coverage.probability

32. theorem OAI.CoordinateSweeps.Coverage.probability_many_hits_le_rpow line 507
33. def OAI.CoordinateSweeps.Coverage.encodeSmallSet line 525

    Source comment

    Canonical padded enumeration encodes a subset of size at most r in r optional entries. This supplies the source's (number-of-lines+1)^r union count.

    def encodeSmallSet {L : Type*} [Fintype L] [DecidableEq L] (r : ℕ)
        (S : {S : Finset L // S.card ≤ r}) : Fin r → Option L := fun i =>
    …

34. theorem OAI.CoordinateSweeps.Coverage.mem_iff_encodeSmallSet line 531
35. theorem OAI.CoordinateSweeps.Coverage.encodeSmallSet_injective line 550
36. theorem OAI.CoordinateSweeps.Coverage.card_smallSets_le line 558
37. theorem OAI.CoordinateSweeps.Coverage.probability_smallSet_hits_le line 565

    Source comment

    Uniform union bound over small sets of lines, without conditioning on a set chosen from the particle array.

    theorem probability_smallSet_hits_le {L : Type*} [Fintype L] [DecidableEq L]
        (w : X → ℝ) (hw : ∀ x, 0 ≤ w x) (hs : ∑ x, w x = 1) (line : X → L)
        (r : ℕ) (p : ℝ) (hp : 0 ≤ p) (hp1 : p ≤ 1)
        (hprob : ∀ S : Finset L, S.card ≤ r → (∑ x, if line x ∈ S then w x else 0) ≤ p)
        (u : ℝ) (hu : 0 ≤ u) :
        probability w (fun x : I → X => ∃ S : Finset L, S.card ≤ r ∧
          u ≤ ((Finset.univ.filter (fun i => line (x i) ∈ S)).card : ℝ)) ≤
          ((Fintype.card L+1 : ℕ) : ℝ)^r * (2 : ℝ)^Fintype.card I * p^u := by
    …

    Mentions: OAI.CoordinateSweeps.Coverage.probability

38. theorem OAI.CoordinateSweeps.Coverage.sum_lineSet line 603
39. theorem OAI.CoordinateSweeps.Coverage.probability_lineSet_le line 612
40. def OAI.CoordinateSweeps.Coverage.heavySet line 620
41. theorem OAI.CoordinateSweeps.Coverage.heavySet_card_mul_le line 623
42. theorem OAI.CoordinateSweeps.Coverage.heavySet_card_le_floor line 635
43. def OAI.CoordinateSweeps.Coverage.occupancy line 641
44. theorem OAI.CoordinateSweeps.Coverage.sum_occupancy line 645
45. theorem OAI.CoordinateSweeps.Coverage.heavy_occupancy_card_le line 654
46. theorem OAI.CoordinateSweeps.Coverage.probability_heavy_occupancy_le line 661

    Source comment

    Probability of many particles in particle-heavy lines. The random line set is controlled by a union over ALL small deterministic sets.

    theorem probability_heavy_occupancy_le (w : X → ℝ) (hw : ∀ x, 0 ≤ w x)
        (hs : ∑ x, w x = 1) (line : X → L) {v : ℝ} (hv : 0 < v)
        (p δ : ℝ) (hδ : 0 ≤ δ) (hp : 0 ≤ p) (hp1 : p ≤ 1)
        (hline : ∀ l, (∑ x, if line x = l then w x else 0) ≤ δ)
        (hrp : (⌊(Fintype.card I : ℝ)/v⌋₊ : ℝ)*δ ≤ p)
        (u : ℝ) (hu : 0 ≤ u) :
        probability w (fun x : I → X =>
          u ≤ ((Finset.univ.filter (fun i => line (x i) ∈ heavySet (occupancy line x) v)).card : ℝ)) ≤
          ((Fintype.card L+1 : ℕ) : ℝ)^⌊(Fintype.card I : ℝ)/v⌋₊ *
            (2 : ℝ)^Fintype.card I * p^u := by
    …

    Mentions: OAI.CoordinateSweeps.Coverage.probability, OAI.CoordinateSweeps.Coverage.heavySet, OAI.CoordinateSweeps.Coverage.occupancy

47. theorem OAI.CoordinateSweeps.Coverage.probability_or_le line 687
48. theorem OAI.CoordinateSweeps.Coverage.probability_coverage_le_real line 695