OAI/RingTheory/DirectFiniteness/SlabAvoidance.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyCounterexample.FiniteLocalLemma.avoid line 15

   Source documentation

   Avoid a finite list of bad events.

   def avoid (E : ι → Set Ω) (s : Finset ι) : Set Ω := ⋂ i ∈ s, (E i)ᶜ

2. lemma OAI.KaplanskyCounterexample.FiniteLocalLemma.mem_avoid line 17
3. lemma OAI.KaplanskyCounterexample.FiniteLocalLemma.avoid_empty line 20
4. lemma OAI.KaplanskyCounterexample.FiniteLocalLemma.avoid_insert line 25
5. lemma OAI.KaplanskyCounterexample.FiniteLocalLemma.avoid_union line 31
6. lemma OAI.KaplanskyCounterexample.FiniteLocalLemma.avoid_anti line 37
7. lemma OAI.KaplanskyCounterexample.FiniteLocalLemma.measurable_avoid line 45
8. lemma OAI.KaplanskyCounterexample.FiniteLocalLemma.prob_avoid_insert line 52
9. lemma OAI.KaplanskyCounterexample.FiniteLocalLemma.avoid_union_lower line 62

   Source documentation

   Successive avoidance bounds, in multiplication form (no conditional measure or division by a possibly zero probability).

   lemma avoid_union_lower {x : ι → ℝ} (hE : ∀ i, MeasurableSet (E i))
       (hx : ∀ i, 0 ≤ 1 - x i) (s t : Finset ι) (hd : Disjoint s t)
       (hc : ∀ (u : Finset ι), u ⊆ s ∪ t → ∀ i ∈ t, i ∉ u →
         μ.real (E i ∩ avoid E u) ≤ x i * μ.real (avoid E u)) :
       (∏ i ∈ t, (1 - x i)) * μ.real (avoid E s) ≤ μ.real (avoid E (s ∪ t)) := by
   …

   Mentions: OAI.KaplanskyCounterexample.FiniteLocalLemma.avoid

10. theorem OAI.KaplanskyCounterexample.FiniteLocalLemma.asymmetric line 93

    Source documentation

    Product-form asymmetric Lovász local lemma on a finite event list. The independence hypothesis is the usual independence from all non-neighbors jointly, written directly as an equality of real probabilities.

    theorem asymmetric {x : ι → ℝ} (hE : ∀ i, MeasurableSet (E i))
        (hx0 : ∀ i, 0 ≤ x i) (hx1 : ∀ i, x i < 1)
        (Γ : ι → Finset ι)
        (hind : ∀ i (s : Finset ι), i ∉ s → Disjoint s (Γ i) →
          μ.real (E i ∩ avoid E s) = μ.real (E i) * μ.real (avoid E s))
        (hprob : ∀ i, μ.real (E i) ≤ x i * ∏ j ∈ Γ i, (1 - x j)) :
        ∀ s : Finset ι, 0 < μ.real (avoid E s) ∧
          ∀ i ∉ s, μ.real (E i ∩ avoid E s) ≤ x i * μ.real (avoid E s) := by
    …

    Mentions: OAI.KaplanskyCounterexample.FiniteLocalLemma.avoid

11. lemma OAI.KaplanskyCounterexample.FiniteLocalLemma.one_sub_sum_le_prod line 162

    Source documentation

    The elementary product bound used in the weighted local lemma.

    lemma one_sub_sum_le_prod {x : ι → ℝ} (hx0 : ∀ i, 0 ≤ x i)
        (hx1 : ∀ i, x i ≤ 1) (s : Finset ι) :
        1 - ∑ i ∈ s, x i ≤ ∏ i ∈ s, (1 - x i) := by
    …

12. def OAI.KaplanskyCounterexample.FiniteLocalLemma.neighbors line 178

    Source documentation

    The dependency graph obtained by sharing one of the assigned variables.

    def neighbors (deps : ι → Finset κ) (i : ι) : Finset ι :=
    …

13. def OAI.KaplanskyCounterexample.FiniteLocalLemma.load line 182

    Source documentation

    Total event weight at a random variable.

    def load (deps : ι → Finset κ) (w : ι → ℝ) (v : κ) : ℝ :=
    …

14. lemma OAI.KaplanskyCounterexample.FiniteLocalLemma.weight_le_load line 186
15. lemma OAI.KaplanskyCounterexample.FiniteLocalLemma.neighbor_weight_le_loads line 194
16. theorem OAI.KaplanskyCounterexample.FiniteLocalLemma.weighted_four line 214
17. def OAI.KaplanskyCounterexample.FiniteLocalLemma.DeterminedBy line 264

    Source documentation

    An event is determined by a finite set of coordinates.

    def DeterminedBy (f : κ → Ω → β) (s : Finset κ) (A : Set Ω) : Prop :=
    …

18. lemma OAI.KaplanskyCounterexample.FiniteLocalLemma.preimage_image_of_determined line 268
19. lemma OAI.KaplanskyCounterexample.FiniteLocalLemma.determined_avoid line 279
20. lemma OAI.KaplanskyCounterexample.FiniteLocalLemma.measurable_of_determined line 293
21. lemma OAI.KaplanskyCounterexample.FiniteLocalLemma.independent_of_non_neighbors line 301
22. theorem OAI.KaplanskyCounterexample.FiniteLocalLemma.weighted_four_independent line 325
23. theorem OAI.KaplanskyCounterexample.FiniteGeometry.exists_linearEquiv_apply_eq line 347

    Source documentation

    Transitivity on nonzero vectors, proved by extending an isomorphism of one-dimensional subspaces.

    theorem exists_linearEquiv_apply_eq {x y : E} (hx : x ≠ 0) (hy : y ≠ 0) :
        ∃ g : E ≃ₗ[Q] E, g x = y := by
    …

24. abbrev OAI.KaplanskyCounterexample.FiniteGeometry.Plane line 357
25. instance OAI.KaplanskyCounterexample.FiniteGeometry.(instance at line 360) line 360
26. instance OAI.KaplanskyCounterexample.FiniteGeometry.(instance at line 364) line 364
27. def OAI.KaplanskyCounterexample.FiniteGeometry.mapPlane line 369

    Source documentation

    An ambient automorphism permutes the plane sample space.

    def mapPlane (g : E ≃ₗ[Q] E) : Plane Q E ≃ Plane Q E where
    …

    Mentions: OAI.KaplanskyCounterexample.FiniteGeometry.Plane

28. theorem OAI.KaplanskyCounterexample.FiniteGeometry.mem_mapPlane line 381
29. def OAI.KaplanskyCounterexample.FiniteGeometry.planesThroughEquiv line 387

    Source documentation

    The number of planes through a nonzero vector is independent of it.

    def planesThroughEquiv {x y : E} (g : E ≃ₗ[Q] E) (h : g x = y) :
        {P : Plane Q E // x ∈ P.val} ≃ {P : Plane Q E // y ∈ P.val} where
    …

    Mentions: OAI.KaplanskyCounterexample.FiniteGeometry.Plane

30. def OAI.KaplanskyCounterexample.FiniteGeometry.planeNonzeroEquiv line 409

    Source documentation

    Nonzero elements of a plane are precisely its ambient nonzero vectors.

    def planeNonzeroEquiv (P : Plane Q E) :
        {x : P.val // x ≠ 0} ≃ {x : {x : E // x ≠ 0} // x.val ∈ P.val} where
    …

    Mentions: OAI.KaplanskyCounterexample.FiniteGeometry.Plane

31. lemma OAI.KaplanskyCounterexample.FiniteGeometry.card_plane_nonzero line 421
32. lemma OAI.KaplanskyCounterexample.FiniteGeometry.card_relation line 429

    Source documentation

    Double counting of a finite relation.

    lemma card_relation {α : Type u_10} {β : Type u_11} [Fintype α] [Fintype β] (R : α → β → Prop) :
        (∑ a, Fintype.card {b // R a b}) = ∑ b, Fintype.card {a // R a b} := by
    …

33. lemma OAI.KaplanskyCounterexample.FiniteGeometry.card_planesThrough_mul line 437
34. lemma OAI.KaplanskyCounterexample.FiniteGeometry.plane_nonempty line 452
35. lemma OAI.KaplanskyCounterexample.FiniteGeometry.planesThrough_ratio line 458

    Source documentation

    Pure counting form of the inclusion probability.

    lemma planesThrough_ratio [Nonempty (Plane Q E)] {x : E} (hx : x ≠ 0) :
        (Fintype.card {P : Plane Q E // x ∈ P.val} : ℝ) / Fintype.card (Plane Q E) =
          (Fintype.card Q ^ 2 - 1 : ℕ) / (Fintype.card E - 1 : ℕ) := by
    …

    Mentions: OAI.KaplanskyCounterexample.FiniteGeometry.Plane

36. theorem OAI.KaplanskyCounterexample.FiniteGeometry.probability_mem_plane line 469
37. def OAI.KaplanskyCounterexample.FiniteGeometry.inclusionProbability line 496

    Source documentation

    The common one-vector inclusion probability.

    def inclusionProbability (Q : Type u_16) (E : Type u_17) [Field Q] [AddCommGroup E] [Module Q E]
        [Fintype Q] : ℝ :=
    …

38. def OAI.KaplanskyCounterexample.FiniteGeometry.slabMeasure line 501

    Source documentation

    Independent choices of uniformly distributed slab direction planes.

    def slabMeasure : Measure (κ → Plane Q E) :=
    …

    Mentions: OAI.KaplanskyCounterexample.FiniteGeometry.Plane

39. instance OAI.KaplanskyCounterexample.FiniteGeometry.(instance at line 504) line 504
40. def OAI.KaplanskyCounterexample.FiniteGeometry.includesAll line 510

    Source documentation

    Each bad event requires one specified nonzero vector in each of its specified direction planes.

    def includesAll (s : Finset κ) (w : κ → E) : Set (κ → Plane Q E) :=
    …

    Mentions: OAI.KaplanskyCounterexample.FiniteGeometry.Plane

41. lemma OAI.KaplanskyCounterexample.FiniteGeometry.probability_includesAll line 513
42. theorem OAI.KaplanskyCounterexample.FiniteGeometry.exists_slab_assignment line 527