OAI/Analysis/Littlewood/Nibble.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.card_biUnion_upper line 15
2. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.card_biUnion_lower line 23
3. def OAI.AsymptoticallyMinimalLittlewood.Nibble.incident line 48
4. def OAI.AsymptoticallyMinimalLittlewood.Nibble.hits line 51
5. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.mem_incident line 55
6. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.mem_hits line 59
7. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.hits_card_upper line 65
8. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.hits_card_deviation line 70
9. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.residual_test_frequency line 90
10. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.residual_degree_variance line 99

    Source documentation

    Codegrees control the influence of each edge-bit on a residual degree.

    lemma residual_degree_variance (U : Finset V) (S : Finset E) (A : E → Finset V)
        {r : ℕ} {D C p : ℝ} (hD : 0 ≤ D) (hC : 0 ≤ C)
        (hp : 0 ≤ p) (hp1 : p ≤ 1)
        (hsub : ∀ e ∈ S, A e ⊆ U) (hr : ∀ e ∈ S, (A e).card ≤ r)
        (hdeg : ∀ v ∈ U, ((incident S A v).card : ℝ) ≤ D)
        (hcodeg : ∀ v ∈ U, ∀ w ∈ U, v ≠ w →
          ((incident S A v ∩ incident S A w).card : ℝ) ≤ C)
        (v : V) (hv : v ∈ U) :
        let Y : (E → Bool) → ℝ := fun s ↦
    …

    Mentions: OAI.AsymptoticallyMinimalLittlewood.Nibble.incident

11. def OAI.AsymptoticallyMinimalLittlewood.Nibble.untouched line 138

    Source documentation

    Count the vertices missed by the selected edges.

    def untouched (U : Finset V) (S : Finset E) (A : E → Finset V) (s : E → Bool) : Finset V :=
    …

12. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.untouched_card line 141
13. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.untouched_variance line 146
14. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.untouched_mean_upper line 167
15. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.residual_degree_mean line 188
16. def OAI.AsymptoticallyMinimalLittlewood.Nibble.restrictEdges line 232

    Source documentation

    Edges remaining after a vertex deletion.

    def restrictEdges (S : Finset E) (A : E → Finset V) (W : Finset V) : Finset E :=
    …

17. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.incident_restrict line 236
18. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.residual_degree_eq line 241
19. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.degree_loss_deleting line 269
20. def OAI.AsymptoticallyMinimalLittlewood.Nibble.isolated line 302

    Source documentation

    The selected edges that meet no other selected edge.

    def isolated (S : Finset E) (A : E → Finset V) (s : E → Bool) : Finset E :=
    …

21. def OAI.AsymptoticallyMinimalLittlewood.Nibble.colliding line 305
22. def OAI.AsymptoticallyMinimalLittlewood.Nibble.collisionCount line 308
23. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.collisionCount_nonneg line 313
24. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.collisionCount_mean line 323
25. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.colliding_card_le line 351
26. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.isolated_pairwise line 388
27. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.isolated_untouched_disjoint line 395
28. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.wasted_vertices_le line 405
29. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.nibble_budget_inequalities line 439
30. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.nibble_bad_loss line 464
31. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.residual_mean_estimate line 472
32. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.incident_restrict_subset line 532
33. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.one_round line 537
34. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.incident_mono line 694
35. structure OAI.AsymptoticallyMinimalLittlewood.Nibble.PackingState line 701

    Source documentation

    The bookkeeping invariant of a partial matching and its active graph.

    structure PackingState (U : Finset V) (S : Finset E) (A : E → Finset V) where
    …

36. def OAI.AsymptoticallyMinimalLittlewood.Nibble.PackingState.initial line 714
37. def OAI.AsymptoticallyMinimalLittlewood.Nibble.PackingState.compose line 726
38. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.PackingState.compose_waste line 754
39. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.nibble_iteration line 771

    Source documentation

    Iteration with stopping when the requested small residual has already been reached. All choices are finite and use the one-round theorem.

    lemma nibble_iteration (U : Finset V) (S : Finset E) (A : E → Finset V)
        {r : ℕ} (hr0 : 1 ≤ r) (k : ℕ) {D ε C a K d : ℝ}
        (hD : 0 < D) (he : 0 ≤ ε) (hC : 0 ≤ C)
        (ha : 0 < a) (ha16 : a ≤ 1/16) (hra : (r : ℝ)*a ≤ 1/4)
        (hK : 0 ≤ K) (_hd : 0 < d)
        (hDmin : 1 ≤ (1-((r-1 : ℕ) : ℝ)*a)^k*D)
        (hecap : (1+2*(r : ℝ)*a)^k*(ε+8*(r : ℝ)^2*a^2*D*k) ≤
          (1-((r-1 : ℕ) : ℝ)*a)^k*D/4)
        (hCmin : C ≤ a*((1-((r-1 : ℕ) : ℝ)*a)^k*D))
        (hcode : U.card*C ≤ K*((1-((r-1 : ℕ) : ℝ)*a)^k*D))
        (hsize : 512*(r : ℝ) ≤ a*d*U.card)
        (hmany : 16*(r : ℝ)^2*(K+1)^2 ≤ a^5*d*U.card)
    …

40. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.nibble_parameters line 922

    Source documentation

    Fixed nibble parameters, chosen in the order required by packing: first the tolerated residual, then finitely many rounds, then regularity.

    lemma nibble_parameters (r : ℕ) {d : ℝ} (hd : 0 < d) :
        ∃ (a : ℝ) (k : ℕ) (e : ℝ), 0 < a ∧ a ≤ 1/16 ∧
          (r : ℝ)*a ≤ 1/4 ∧ 0 < e ∧
          0 < (1-((r-1 : ℕ) : ℝ)*a)^k ∧
          (1+2*(r : ℝ)*a)^k*(e+8*(r : ℝ)^2*a^2*k) ≤
            (1-((r-1 : ℕ) : ℝ)*a)^k/4 ∧
          (1-a/2)^k ≤ d ∧ k*(16*(r : ℝ)+1)*a^2 ≤ d := by
    …

41. theorem OAI.AsymptoticallyMinimalLittlewood.Nibble.almost_perfect_matching line 991