RamseyThinning.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.SeparableQuotient.InfiniteRamsey.eventually_constant line 13
def OAI.SeparableQuotient.InfiniteRamsey.limitColor line 17
lemma OAI.SeparableQuotient.InfiniteRamsey.limitColor_eventually line 21
theorem OAI.SeparableQuotient.InfiniteRamsey.homogeneous line 28
Source documentation
The finite-set form of the infinite Ramsey theorem, proved by iterated ultrafilter colors. Used only for the four-hit thinning in exact-pairs.
```
theorem homogeneous (n : ℕ) (c : Finset ℕ → χ) :
    ∃ (M : Set ℕ) (b : χ), M.Infinite ∧
      ∀ s : Finset ℕ, (↑s : Set ℕ) ⊆ M → s.card = n → c s = b := by
…
```

theorem OAI.SeparableQuotient.InfiniteRamsey.homogeneous_subset line 102

Source documentation

Relative version for any infinite subset of the natural numbers.

theorem homogeneous_subset (n : ℕ) (c : Finset ℕ → χ) (A : Set ℕ) (hA : A.Infinite) :
    ∃ (M : Set ℕ) (b : χ), M ⊆ A ∧ M.Infinite ∧
      ∀ s : Finset ℕ, (↑s : Set ℕ) ⊆ M → s.card = n → c s = b := by
…

lemma OAI.SeparableQuotient.ActualSpace.four_distinct_finset line 136

theorem OAI.SeparableQuotient.ActualSpace.four_hits_thinning line 144

Source documentation

Four-hit thinning under the Type I partition estimate.

theorem four_hits_thinning {f : Family} (x : ℕ → Γ →₀ ℝ) (J T : ℕ → ℕ)
    (hJT : ∀ i, J i ≤ T i)
    (horder : ∀ i j, i < j → T i < J j)
    (hs : ∀ i j, i < j → ∀ a ∈ (x i).support, ∀ b ∈ (x j).support, a < b)
    (hcoh : ∀ i j, i < j → ∀ a ∈ (x i).support, ∀ b ∈ (x i).support,
      rho (min a b) (max a b) ≤ J j)
    (M A δ : ℝ) (hM : ∀ i, ‖norming.includeFinite (x i)‖ ≤ M) (hA : 0 ≤ A) (hδ : 0 < δ)
    (hlow : ∀ i (e : TypeI f), (∀ j, e.child j ∈ f.norming) → e.weight < J i →
      |norming.evaluateArray (norming.includeFinite (x i)) e.value| ≤ A * f.theta e.weight)
    (htail : Tendsto (fun i => vectorL1 (x i) * tail (fun j => 1 / (f.m j : ℝ)) (T i+1)) atTop (𝓝 0))
    (hnull : ∀ Q : InfinitePath f, Tendsto (fun i => pathFunctional Q (norming.includeFinite (x i))) atTop (𝓝 0))
    (N : Set ℕ) (hN : N.Infinite) :
…

Mentions: OAI.SeparableQuotient.ActualSpace.e, OAI.SeparableQuotient.ActualSpace.vectorL1, OAI.SeparableQuotient.ActualSpace.pathFunctional