OAI/Analysis/CircleDomains/Selection/FourSampleBound.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The four independent samples in the alternating collar argument. Outer measure suffices, so no extra measurability premise is imposed on meeting events.

  1. def OAI.CircleDomainRigidity.pairSample line 17
  2. def OAI.CircleDomainRigidity.crossSample line 19
  3. theorem OAI.CircleDomainRigidity.measurePreserving_pairSample line 22
  4. theorem OAI.CircleDomainRigidity.measurePreserving_crossSample line 38
  5. theorem OAI.CircleDomainRigidity.four_cross_pair_union_bound line 43
  6. theorem OAI.CircleDomainRigidity.four_sample_rectangle_lower_bound line 61
  7. theorem OAI.CircleDomainRigidity.four_sample_meeting_constraint line 72
  8. theorem OAI.CircleDomainRigidity.exists_small_crossing_budget line 84

    Source documentation

    A single sufficiently small collar budget defeats the four-sample lower bound.

    theorem exists_small_crossing_budget (C : ℝ≥0∞) (hC : C ≠ ∞) :
    ∃ δ : ℝ≥0∞, 0 < δ ∧
      4 * (2 * δ + (1 + C) * δ ^ 2) < (1 / 10 : ℝ≥0∞) ^ 4 := by
…