OAI/Analysis/SeparableQuotients/Parameters.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SeparableQuotient.Parameters.d line 12
  2. def OAI.SeparableQuotient.Parameters.state line 15

    Source documentation

    State stores the exponent scale and twice the sum of all earlier lengths.

    def state (s : ℕ) : ℕ → ℕ × ℕ
  | 0 => ((d 0 + 1) + 1 + d 0 + (d 0)^2, 0)
  | n+1 =>
    let old := state s n
…

    Mentions: OAI.SeparableQuotient.Parameters.d

  3. def OAI.SeparableQuotient.Parameters.t line 22
  4. def OAI.SeparableQuotient.Parameters.B line 23
  5. def OAI.SeparableQuotient.Parameters.L line 24
  6. def OAI.SeparableQuotient.Parameters.m line 25
  7. def OAI.SeparableQuotient.Parameters.r line 26
  8. def OAI.SeparableQuotient.Parameters.q line 27
  9. def OAI.SeparableQuotient.Parameters.theta line 28
  10. lemma OAI.SeparableQuotient.Parameters.B_zero line 30
  11. lemma OAI.SeparableQuotient.Parameters.B_succ line 31
  12. lemma OAI.SeparableQuotient.Parameters.t_succ line 32
  13. lemma OAI.SeparableQuotient.Parameters.d_pos line 35
  14. lemma OAI.SeparableQuotient.Parameters.L_pos line 36
  15. lemma OAI.SeparableQuotient.Parameters.m_pos line 37
  16. lemma OAI.SeparableQuotient.Parameters.t_bound line 39
  17. lemma OAI.SeparableQuotient.Parameters.t_square line 44
  18. lemma OAI.SeparableQuotient.Parameters.t_pos line 49
  19. lemma OAI.SeparableQuotient.Parameters.t_strict line 53
  20. lemma OAI.SeparableQuotient.Parameters.B_eq_sum line 59
  21. lemma OAI.SeparableQuotient.Parameters.L_strict line 64
  22. lemma OAI.SeparableQuotient.Parameters.m_strict line 69
  23. lemma OAI.SeparableQuotient.Parameters.theta_numerator line 77
  24. lemma OAI.SeparableQuotient.Parameters.theta_eq line 88
  25. lemma OAI.SeparableQuotient.Parameters.length_qprime_power line 95
  26. lemma OAI.SeparableQuotient.Parameters.ratio_eq line 104
  27. lemma OAI.SeparableQuotient.Parameters.depth_integer_bound line 114
  28. lemma OAI.SeparableQuotient.Parameters.depth_bound line 143
  29. lemma OAI.SeparableQuotient.Parameters.depth_theta_bound line 150
  30. lemma OAI.SeparableQuotient.Parameters.hasSum_theta line 155
  31. lemma OAI.SeparableQuotient.Parameters.theta_sum_small line 166
  32. lemma OAI.SeparableQuotient.Parameters.theta_tail line 170
  33. lemma OAI.SeparableQuotient.Parameters.reciprocal_le_theta line 185
  34. lemma OAI.SeparableQuotient.Parameters.reciprocal_sum_small line 191
  35. lemma OAI.SeparableQuotient.Parameters.d_div_t_tendsto line 199
  36. lemma OAI.SeparableQuotient.Parameters.log_ratio_eq line 210
  37. lemma OAI.SeparableQuotient.Parameters.parameter_growth line 222
  38. lemma OAI.SeparableQuotient.Parameters.ratio_tendsto_atTop line 229
  39. lemma OAI.SeparableQuotient.Parameters.s_r_conjugate line 242
  40. lemma OAI.SeparableQuotient.Parameters.sNext_q_conjugate line 245
  41. lemma OAI.SeparableQuotient.Parameters.q_bounds line 250
  42. def OAI.SeparableQuotient.Colors.partitionEquiv line 267

    Source documentation

    A partition of ω₁ into countably many unbounded fibers.

    def partitionEquiv : OmegaOne.{0} ≃ ℕ × OmegaOne.{0} :=
…
  43. def OAI.SeparableQuotient.Colors.color line 272
  44. def OAI.SeparableQuotient.Colors.inColor line 274
  45. lemma OAI.SeparableQuotient.Colors.color_inColor line 276
  46. lemma OAI.SeparableQuotient.Colors.inColor_injective line 279
  47. lemma OAI.SeparableQuotient.Colors.fiber_unbounded line 284