OAI/Analysis/SeparableQuotients/WindowEstimates.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SeparableQuotient.SeriesTails.tail line 11
2. lemma OAI.SeparableQuotient.SeriesTails.tendsto_tail line 13
3. lemma OAI.SeparableQuotient.SeriesTails.tail_nonneg line 16
4. lemma OAI.SeparableQuotient.SeriesTails.sum_le_tail line 19
5. lemma OAI.SeparableQuotient.ActualSpace.evaluateArray_finite line 44
6. def OAI.SeparableQuotient.ActualSpace.vectorL1 line 60
7. lemma OAI.SeparableQuotient.ActualSpace.vectorL1_nonneg line 62
8. lemma OAI.SeparableQuotient.ActualSpace.typeI_eval_le_l1 line 65
9. lemma OAI.SeparableQuotient.ActualSpace.path_piece_zero_of_earlier_hit line 81
10. lemma OAI.SeparableQuotient.Norming.Family.theta_summable line 103
11. lemma OAI.SeparableQuotient.Norming.Family.m_inv_summable line 107
12. lemma OAI.SeparableQuotient.SeriesTails.sum_outside_window_bound line 116
13. lemma OAI.SeparableQuotient.ActualSpace.finitePathFunctional_apply line 178
14. lemma OAI.SeparableQuotient.ActualSpace.window_error_bound line 182
15. lemma OAI.SeparableQuotient.CoverRecurrence.recurrent_of_covers line 214

    Source documentation

    Uniformly finite covers of all initial segments give a single sequence of covering objects which eventually hits every member of an infinite fixed set. No compactness of the covering objects themselves is assumed.

    lemma recurrent_of_covers {Λ : Type*} (Hit : Λ → ℕ → Prop) (D : ℕ)
        (hcover : ∀ n, ∃ R : Finset Λ, R.card ≤ D ∧ ∀ i ≤ n, ∃ P ∈ R, Hit P i) :
        ∃ (P : ℕ → Λ) (W : Set ℕ), W.Infinite ∧ ∀ i ∈ W, ∀ᶠ n in atTop, Hit (P n) i := by
    …

16. lemma OAI.SeparableQuotient.ActualSpace.not_all_four_hits line 256

    Source documentation

    Pathwise nullity excludes four recurrent hits by reconstruction of a limiting infinite path.

    lemma not_all_four_hits {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)) :
        ¬ (∀ w v t k : ℕ, w < v → v < t → t < k →
    …

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