FatouSelection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

One compatible sample with arbitrarily late good widths

The grid shifts must be fixed before the staircase width is chosen. Fatou's lemma preserves a strict expected-cost budget along a sequence of widths, and yields infinitely many good widths for one fixed sample.

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_compatible_frequently_small_cost line 19

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_compatible_frequently_small_pair line 42

Source documentation

The second cost is independent of the width, so the same sample has a small terminal cost and arbitrarily late small wedge costs.

theorem exists_compatible_frequently_small_pair
    {X : Type*} [MeasurableSpace X] {μ : Measure X} [IsProbabilityMeasure μ]
    (W : ℕ → X → ℝ≥0∞) (J : X → ℝ≥0∞)
    (hW : ∀ n, AEMeasurable (W n) μ) (hJ : AEMeasurable J μ)
    {P : X → Prop} (hP : ∀ᵐ x ∂μ, P x) {c : ℝ≥0∞} (hc : c < 1)
    (hmean : ∀ n, (∫⁻ x, W n x + J x ∂μ) ≤ c) :
    ∃ x, P x ∧ J x < 1 ∧ ∃ᶠ n in atTop, W n x < 1 := by
…