OAI/RingTheory/DirectFiniteness/Alteration.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KaplanskyCounterexample.FiniteGeometry.selectionMeasure line 15

    Source documentation

    Independent selection of points at a prescribed probability.

    def selectionMeasure (p : Set.Icc (0 : ℝ) 1) : Measure (α → Bool) :=
…
  2. instance OAI.KaplanskyCounterexample.FiniteGeometry.(instance at line 18) line 18
  3. def OAI.KaplanskyCounterexample.FiniteGeometry.allSelected line 22
  4. lemma OAI.KaplanskyCounterexample.FiniteGeometry.probability_allSelected line 24
  5. lemma OAI.KaplanskyCounterexample.FiniteGeometry.integral_selection_indicator line 36
  6. theorem OAI.KaplanskyCounterexample.FiniteGeometry.exists_avoiding_card line 49

    Source documentation

    Finite probabilistic alteration: delete all vertices in every fully chosen forbidden set. Duplicate forbidden sets are permitted, and only strengthen the upper bound on expected deletions.

    theorem exists_avoiding_card [Fintype ι] (C : ι → Finset α)
    (hne : ∀ i, (C i).Nonempty) (p : Set.Icc (0 : ℝ) 1) :
    ∃ O : Finset α, (∀ i, ¬ C i ⊆ O) ∧
      (Fintype.card α : ℝ) * p.val - ∑ i, (C i).card * p.val ^ (C i).card ≤ O.card := by
…