OAI/Combinatorics/InfiniteMatroid/Interpolation.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InfiniteMatroidCounterexample.AgreeBelow line 13

   Source documentation

   Two subsets of ℕ agree on the first m labels.

   def AgreeBelow (X Y : Set ℕ) (m : ℕ) : Prop :=
   …

2. def OAI.InfiniteMatroidCounterexample.CylinderContinuous line 16
3. def OAI.InfiniteMatroidCounterexample.deletePrefix line 23

   Source documentation

   Delete, in the usual order of ℕ, the labels not reserved by the lower endpoint or by the finite prefix.

   def deletePrefix (I X : Set ℕ) (m k : ℕ) : Set ℕ :=
   …

4. lemma OAI.InfiniteMatroidCounterexample.deletePrefix_zero line 26
5. lemma OAI.InfiniteMatroidCounterexample.subset_deletePrefix line 30
6. lemma OAI.InfiniteMatroidCounterexample.deletePrefix_subset line 35
7. lemma OAI.InfiniteMatroidCounterexample.deletePrefix_antitone line 38
8. lemma OAI.InfiniteMatroidCounterexample.deletePrefix_agree line 46
9. lemma OAI.InfiniteMatroidCounterexample.deletePrefix_step line 51
10. lemma OAI.InfiniteMatroidCounterexample.deletePrefix_finite line 63
11. def OAI.InfiniteMatroidCounterexample.deleteTail line 72

    Source documentation

    The limit after every eligible label has been deleted.

    def deleteTail (I X : Set ℕ) (m : ℕ) : Set ℕ :=
    …

12. lemma OAI.InfiniteMatroidCounterexample.subset_deleteTail line 75
13. lemma OAI.InfiniteMatroidCounterexample.deleteTail_subset line 78
14. lemma OAI.InfiniteMatroidCounterexample.deleteTail_finite line 81
15. lemma OAI.InfiniteMatroidCounterexample.deletePrefix_agree_tail line 87
16. lemma OAI.InfiniteMatroidCounterexample.deletion_stage line 102

    Source documentation

    One stage of the infinite-endpoint interpolation: the stopping time is finite, all late probes are reset above -1, and earlier probes lose less than the prescribed tolerance.

    lemma deletion_stage
        {f : ℕ → Set ℕ → ℝ} {I Y X : Set ℕ}
        (hcc : CylinderContinuous f I Y)
        (hone : ∀ n A B, I ⊆ A → A ⊆ B → B ⊆ Y →
          (∃ e, B ⊆ insert e A) → f n B ≤ f n A + 1)
        (hlow : ∀ Z, I ⊆ Z → Z ⊆ Y → (Z \ I).Finite →
          ∀ j, ∃ n ≥ j, f n Z < 0)
        (hIX : I ⊆ X) (hXY : X ⊆ Y) (j : ℕ) (ε : ℝ) (hε : 0 < ε) :
        ∃ Z, I ⊆ Z ∧ Z ⊆ X ∧ (X \ Z).Finite ∧
          (∃ n ≥ j, f n Z ≤ 0) ∧
          (∀ n < j, |f n X - f n Z| < ε) ∧
          (Z = X ∨ ∀ n ≥ j, -1 ≤ f n Z) := by
    …

    Mentions: OAI.InfiniteMatroidCounterexample.CylinderContinuous

17. lemma OAI.InfiniteMatroidCounterexample.antitone_agree_iInter line 164
18. lemma OAI.InfiniteMatroidCounterexample.CylinderContinuous.tendsto_iInter line 188
19. lemma OAI.InfiniteMatroidCounterexample.infinite_endpoint_interpolation line 202
20. def OAI.InfiniteMatroidCounterexample.probeLiminf line 303

    Source documentation

    Extended lower limiting value of the real probes.

    noncomputable def probeLiminf {α : Type*} (f : ℕ → Set α → ℝ) (X : Set α) : EReal :=
    …

21. lemma OAI.InfiniteMatroidCounterexample.ereal_liminf_add_real line 306
22. lemma OAI.InfiniteMatroidCounterexample.probeLiminf_finite_change line 315
23. lemma OAI.InfiniteMatroidCounterexample.probeLiminf_mono line 322
24. lemma OAI.InfiniteMatroidCounterexample.probeLiminf_le_zero line 327
25. lemma OAI.InfiniteMatroidCounterexample.probeLiminf_ge_neg_one line 333
26. def OAI.InfiniteMatroidCounterexample.LowerBasis line 353

    Source documentation

    The half-closed interval used by the lower-limit rule.

    def LowerBasis {α : Type*} (f : ℕ → Set α → ℝ) (X : Set α) : Prop :=
    …

27. lemma OAI.InfiniteMatroidCounterexample.infinite_endpoint_liminf_interpolation line 356
28. def OAI.InfiniteMatroidCounterexample.IntervalFiniteShift line 379

    Source documentation

    Exact finite-cardinality translation on a fixed interval.

    def IntervalFiniteShift {α : Type*} (f : ℕ → Set α → ℝ) (I Y : Set α) : Prop :=
    …

29. lemma OAI.InfiniteMatroidCounterexample.finite_lower_interpolation line 383
30. lemma OAI.InfiniteMatroidCounterexample.finite_upper_interpolation line 429
31. lemma OAI.InfiniteMatroidCounterexample.local_interpolation line 470

    Source documentation

    The complete local interpolation argument, including both finite rounding cases and the opposite-infinite-endpoint case.

    lemma local_interpolation
        {f : ℕ → Set ℕ → ℝ} {I Y : Set ℕ} (hIY : I ⊆ Y)
        (hcc : CylinderContinuous f I Y)
        (hmono : ∀ n A B, I ⊆ A → A ⊆ B → B ⊆ Y → f n A ≤ f n B)
        (hone : ∀ n A B, I ⊆ A → A ⊆ B → B ⊆ Y →
          (∃ e, B ⊆ insert e A) → f n B ≤ f n A + 1)
        (hshift : IntervalFiniteShift f I Y)
        (hlow : probeLiminf f I ≤ -1) (hhigh : 0 < probeLiminf f Y) :
        ∃ B, I ⊆ B ∧ B ⊆ Y ∧ LowerBasis f B := by
    …

    Mentions: OAI.InfiniteMatroidCounterexample.CylinderContinuous, OAI.InfiniteMatroidCounterexample.IntervalFiniteShift, OAI.InfiniteMatroidCounterexample.probeLiminf, OAI.InfiniteMatroidCounterexample.LowerBasis