GridWidthSelection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Fixing grid shifts before the staircase width

The wedge costs depend on a sequence of widths, whereas the terminal cost depends only on the grid shifts. Fatou selection provides one compatible choice of shifts with small terminal cost and arbitrarily late small wedge costs. Thus subsequent collar conditions may impose any finite lower bound on the width-sequence index.

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_compatible_frequently_small_real_pair line 23

Source documentation

The real-valued version of the Fatou selection estimate, with the two costs normalized by their actual thresholds.

theorem exists_compatible_frequently_small_real_pair
    {X : Type*} [MeasurableSpace X] {μ : Measure X} [IsProbabilityMeasure μ]
    (W : ℕ → X → ℝ) (J : X → ℝ) {P : X → Prop} {A B : ℝ}
    (hA : 0 < A) (hB : 0 < B)
    (hWi : ∀ k, Integrable (W k) μ) (hJi : Integrable J μ)
    (hW0 : ∀ k, ∀ᵐ x ∂μ, 0 ≤ W k x) (hJ0 : ∀ᵐ x ∂μ, 0 ≤ J x)
    (hP : ∀ᵐ x ∂μ, P x)
    (hWmean : ∀ k, (∫ x, W k x ∂μ) < A / 4)
    (hJmean : (∫ x, J x ∂μ) < B / 4) :
    ∃ x, P x ∧ J x < B ∧ ∃ᶠ k in atTop, W k x < A := by
…

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_reciprocal_grid_with_frequently_small_widths line 67

Source documentation

Simultaneous choice of reciprocal grid spacing and fixed shifts, retaining any conull compatibility event and arbitrarily late good width indices. The terminal cost includes all compulsory indices.

theorem exists_reciprocal_grid_with_frequently_small_widths {n : ℕ}
    (W : ℕ → ℕ → (Fin n → ℝ) → ℝ) (J : ℕ → (Fin n → ℝ) → ℝ)
    (P : ℕ → (Fin n → ℝ) → Prop) {η δ : ℝ} (hη : 0 < η) (hδ : 0 < δ)
    (hWi : ∀ N k, Integrable (W N k) (reciprocalGridLaw n N))
    (hJi : ∀ N, Integrable (J N) (reciprocalGridLaw n N))
    (hW0 : ∀ N k, ∀ᵐ θ ∂reciprocalGridLaw n N, 0 ≤ W N k θ)
    (hJ0 : ∀ N, ∀ᵐ θ ∂reciprocalGridLaw n N, 0 ≤ J N θ)
    (hP : ∀ N, ∀ᵐ θ ∂reciprocalGridLaw n N, P N θ)
    (hWmean : ∀ᶠ N in atTop, ∀ k,
      (∫ θ, W N k θ ∂reciprocalGridLaw n N) < η / 4)
    (hJmean : Tendsto
      (fun N => reciprocalGridStep N ^ 2 * (∫ θ, J N θ ∂reciprocalGridLaw n N))
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.reciprocalGridLaw, OAI.CircleDomainRigidity.FiniteTransfer.reciprocalGridStep