OAI/Analysis/SeparableQuotients/WindowThinning.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SeparableQuotient.ActualSpace.FamilyL_mono line 11
  2. lemma OAI.SeparableQuotient.ActualSpace.tail_sub_mul_le line 15
  3. structure OAI.SeparableQuotient.ActualSpace.WindowBlocks line 29

    Source documentation

    Window blocks with partition estimates, pathwise nullity, and coherent support bounds.

    structure WindowBlocks {f : Family} (z : BlockSequence f) (J : ℕ) (ε : ℝ) (a : ℕ) where
…

    Mentions: OAI.SeparableQuotient.ActualSpace.BlockSequence

  4. lemma OAI.SeparableQuotient.ActualSpace.exists_windowBlocks line 46
  5. lemma OAI.SeparableQuotient.ActualSpace.WindowBlocks.four_hits line 132
  6. structure OAI.SeparableQuotient.AdaptiveThinning.Step line 151
  7. lemma OAI.SeparableQuotient.AdaptiveThinning.exists_step line 161
  8. def OAI.SeparableQuotient.AdaptiveThinning.choice line 170
  9. structure OAI.SeparableQuotient.AdaptiveThinning.State line 173
  10. def OAI.SeparableQuotient.AdaptiveThinning.initial line 180
  11. def OAI.SeparableQuotient.AdaptiveThinning.next line 184
  12. lemma OAI.SeparableQuotient.AdaptiveThinning.next_mem line 188
  13. lemma OAI.SeparableQuotient.AdaptiveThinning.next_subset line 191
  14. def OAI.SeparableQuotient.AdaptiveThinning.state line 194
  15. lemma OAI.SeparableQuotient.AdaptiveThinning.index_strict line 198
  16. lemma OAI.SeparableQuotient.AdaptiveThinning.rest_antitone line 203
  17. lemma OAI.SeparableQuotient.AdaptiveThinning.later_mem line 208
  18. theorem OAI.SeparableQuotient.AdaptiveThinning.exists_adaptive line 218

    Source documentation

    Repeated infinite thinning where the new relation can depend on the already selected index and its position. No uniform-threshold or countability assumption on the predicate R is required.

    theorem exists_adaptive : ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∃ W : ℕ → Set ℕ,
    (∀ n, R n (φ n) (W n)) ∧ (∀ n m, n < m → φ m ∈ W n) := by
…
  19. def OAI.SeparableQuotient.ActualSpace.WindowBlocks.subsequence line 230
  20. structure OAI.SeparableQuotient.ActualSpace.ThinnedWindows line 248

    Source documentation

    Successively thinned windows. The threshold indexed by n is used strictly after n.

    structure ThinnedWindows {f : Family} (z : BlockSequence f) (J : ℕ) (ε : ℝ) (a : ℕ)
    extends WindowBlocks z J ε a where
…

    Mentions: OAI.SeparableQuotient.ActualSpace.BlockSequence, OAI.SeparableQuotient.ActualSpace.WindowBlocks

  21. lemma OAI.SeparableQuotient.ActualSpace.exists_thinnedWindows line 258
  22. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.hits_after_le_three line 297