OAI/Dynamics/SmoothObstruction/WordParameters.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothObstruction.WordParameters.ell line 12

    Source documentation

    The source logarithm is binary. Levels here are numbered i+1.

    noncomputable def ell (s : ℕ) : ℝ := Real.logb 2 ((2 : ℝ) ^ (2 * s) - 1)
  2. def OAI.SmoothObstruction.WordParameters.K line 13
  3. def OAI.SmoothObstruction.WordParameters.epsilon line 14
  4. def OAI.SmoothObstruction.WordParameters.X line 15
  5. def OAI.SmoothObstruction.WordParameters.nextS line 16
  6. def OAI.SmoothObstruction.WordParameters.sequence line 17
  7. lemma OAI.SmoothObstruction.WordParameters.epsilon_pos line 21
  8. lemma OAI.SmoothObstruction.WordParameters.epsilon_succ line 22
  9. lemma OAI.SmoothObstruction.WordParameters.ell_zero line 27
  10. lemma OAI.SmoothObstruction.WordParameters.ell_bounds line 28
  11. lemma OAI.SmoothObstruction.WordParameters.ell_nonneg line 47
  12. lemma OAI.SmoothObstruction.WordParameters.K_bounds line 55
  13. lemma OAI.SmoothObstruction.WordParameters.polynomial_budget line 67

    Source documentation

    A single integer estimate proves all the logarithmic polynomial budgets at the fixed initial threshold. No floating-point certificate is used.

    lemma polynomial_budget : ∀ k : ℕ, 256 ≤ k → ((k : ℝ) + 14) ^ 16 ≤ (2 : ℝ) ^ k := by
…
  14. lemma OAI.SmoothObstruction.WordParameters.polynomial_root_budget line 83
  15. lemma OAI.SmoothObstruction.WordParameters.rounding line 114
  16. lemma OAI.SmoothObstruction.WordParameters.exp_half_sub_one line 130
  17. lemma OAI.SmoothObstruction.WordParameters.X_lower line 139
  18. theorem OAI.SmoothObstruction.WordParameters.one_step_growth line 153

    Source documentation

    Growth from exactly the source recursion, including the floor to the largest even dimension. No later enlargement of the initial alphabet occurs.

    theorem one_step_growth {i s : ℕ} (hk : 256 ≤ K s) (hε : 32 ≤ epsilon i * K s) :
    6 ≤ X i s ∧ (2 : ℝ) ^ K s ≤ ell (nextS i s) ∧
      (2 : ℝ) ^ ((K s : ℝ) / 3) ≤ K (nextS i s) ∧
      K s ^ 2 ≤ K (nextS i s) ∧ 4 * K s ≤ K (nextS i s) := by
…

    Mentions: OAI.SmoothObstruction.WordParameters.K, OAI.SmoothObstruction.WordParameters.epsilon, OAI.SmoothObstruction.WordParameters.X, OAI.SmoothObstruction.WordParameters.ell, OAI.SmoothObstruction.WordParameters.nextS

  19. theorem OAI.SmoothObstruction.WordParameters.sequence_growth line 184

    Source documentation

    All levels obey the fixed initial threshold and the exact epsilon growth bound in source (word-growth). Level zero means manuscript level one.

    theorem sequence_growth {s₀ : ℕ} (h₀ : 256 ≤ K s₀) :
    ∀ i, 256 ≤ K (sequence s₀ i) ∧
      32 * (2 : ℝ) ^ i ≤ epsilon i * K (sequence s₀ i) := by
…

    Mentions: OAI.SmoothObstruction.WordParameters.K, OAI.SmoothObstruction.WordParameters.sequence, OAI.SmoothObstruction.WordParameters.epsilon

  20. def OAI.SmoothObstruction.WordParameters.commonBound line 211
  21. lemma OAI.SmoothObstruction.WordParameters.common_bound line 214
  22. lemma OAI.SmoothObstruction.WordParameters.log_tolerance line 236
  23. lemma OAI.SmoothObstruction.WordParameters.filter_exponent line 244

    Source documentation

    The logarithmic filter budget at consecutive source levels.

    lemma filter_exponent {i s : ℕ} (hk : 256 ≤ K s) (hε : 32 ≤ epsilon i * K s) :
    Real.logb 2 (10000 : ℝ) + K s +
      (2 : ℝ) ^ (K s / 8) * ell s / 2 -
      ((K (nextS i s) - K (nextS i s) / 2 : ℕ) : ℝ) / 2 ≤
      -(1 / 8 : ℝ) * (2 : ℝ) ^ ((K s : ℝ) / 3) := by
…

    Mentions: OAI.SmoothObstruction.WordParameters.K, OAI.SmoothObstruction.WordParameters.epsilon, OAI.SmoothObstruction.WordParameters.ell, OAI.SmoothObstruction.WordParameters.nextS

  24. lemma OAI.SmoothObstruction.WordParameters.window_exponent line 269

    Source documentation

    The logarithmic window budget, with exactly the source cardinalities.

    lemma window_exponent {i s : ℕ} (hk : 256 ≤ K s) (hε : 32 ≤ epsilon i * K s) :
    Real.logb 2 (10000 : ℝ) + K s +
      (2 : ℝ) ^ (K s / 8) * ell s / 2 - ell (nextS i s) / 2 ≤
      -(2 : ℝ) ^ K s / 4 := by
…

    Mentions: OAI.SmoothObstruction.WordParameters.K, OAI.SmoothObstruction.WordParameters.epsilon, OAI.SmoothObstruction.WordParameters.ell, OAI.SmoothObstruction.WordParameters.nextS

  25. lemma OAI.SmoothObstruction.WordParameters.distance_exponent line 293
  26. def OAI.SmoothObstruction.WordParameters.alphabetSize line 310
  27. def OAI.SmoothObstruction.WordParameters.filterBudget line 311
  28. def OAI.SmoothObstruction.WordParameters.windowBudget line 314
  29. def OAI.SmoothObstruction.WordParameters.distanceBudget line 317
  30. lemma OAI.SmoothObstruction.WordParameters.s_pos_of_Kpos line 322
  31. lemma OAI.SmoothObstruction.WordParameters.alphabetSize_pos line 328
  32. lemma OAI.SmoothObstruction.WordParameters.log_sqrt line 333
  33. lemma OAI.SmoothObstruction.WordParameters.filterBudget_pos line 337
  34. lemma OAI.SmoothObstruction.WordParameters.windowBudget_pos line 342
  35. lemma OAI.SmoothObstruction.WordParameters.distanceBudget_pos line 348
  36. lemma OAI.SmoothObstruction.WordParameters.log_filterBudget line 354
  37. lemma OAI.SmoothObstruction.WordParameters.log_windowBudget line 368
  38. lemma OAI.SmoothObstruction.WordParameters.log_distanceBudget line 382
  39. theorem OAI.SmoothObstruction.WordParameters.actual_budgets line 404

    Source documentation

    All actual probability budgets, not just formal logarithmic surrogates, are controlled at the single fixed initial threshold.

    theorem actual_budgets {i s : ℕ} (hk : 256 ≤ K s) (hε : 32 ≤ epsilon i * K s) :
    filterBudget s (nextS i s) < 1 / 2 ∧
      windowBudget s (nextS i s) < 1 / 4 ∧
      distanceBudget i s (nextS i s) < 1 / 4 := by
…

    Mentions: OAI.SmoothObstruction.WordParameters.K, OAI.SmoothObstruction.WordParameters.epsilon, OAI.SmoothObstruction.WordParameters.filterBudget, OAI.SmoothObstruction.WordParameters.nextS, OAI.SmoothObstruction.WordParameters.windowBudget, OAI.SmoothObstruction.WordParameters.distanceBudget

  40. def OAI.SmoothObstruction.WordParameters.length line 442
  41. def OAI.SmoothObstruction.WordParameters.rate line 446
  42. lemma OAI.SmoothObstruction.WordParameters.length_pos line 448
  43. lemma OAI.SmoothObstruction.WordParameters.length_dvd line 453
  44. lemma OAI.SmoothObstruction.WordParameters.length_eq_pow line 456
  45. lemma OAI.SmoothObstruction.WordParameters.log_length line 462
  46. lemma OAI.SmoothObstruction.WordParameters.step_conditions line 470
  47. lemma OAI.SmoothObstruction.WordParameters.length_ge_two_pow line 477
  48. lemma OAI.SmoothObstruction.WordParameters.length_unbounded line 488
  49. lemma OAI.SmoothObstruction.WordParameters.rate_pos line 492
  50. lemma OAI.SmoothObstruction.WordParameters.rate_step line 499
  51. lemma OAI.SmoothObstruction.WordParameters.rate_step_dyadic line 512
  52. theorem OAI.SmoothObstruction.WordParameters.rate_lower line 526

    Source documentation

    The exact dyadic rate lower bound, with the finite arithmetic sum left unrounded (its value is i(i+21)/2). Level zero is source level one.

    theorem rate_lower {s₀ : ℕ} (h₀ : 256 ≤ K s₀) (i : ℕ) :
    rate s₀ 0 / (2 : ℝ) ^ (∑ j ∈ Finset.range i, (j + 11)) ≤ rate s₀ i := by
…

    Mentions: OAI.SmoothObstruction.WordParameters.K, OAI.SmoothObstruction.WordParameters.rate

  53. lemma OAI.SmoothObstruction.WordParameters.exponent_sum line 534
  54. lemma OAI.SmoothObstruction.WordParameters.K_double_exponential line 540
  55. lemma OAI.SmoothObstruction.WordParameters.double_exp_budget line 553
  56. theorem OAI.SmoothObstruction.WordParameters.rates_not_summable line 568

    Source documentation

    Source divergence: the available-scale information cannot be summable. The proof gives an explicit positive lower bound after level16, not merely an informal comparison of logarithmic growth rates.

    theorem rates_not_summable {s₀ : ℕ} (h₀ : 256 ≤ K s₀) :
    ¬ Summable (fun i => (K (sequence s₀ i) : ℝ) * rate s₀ i ^ 16) := by
…

    Mentions: OAI.SmoothObstruction.WordParameters.K, OAI.SmoothObstruction.WordParameters.sequence, OAI.SmoothObstruction.WordParameters.rate

  57. lemma OAI.SmoothObstruction.WordParameters.initial_threshold line 598

    Source documentation

    A concrete admissible first vector dimension. It makes the main construction's initial-size condition nonvacuous.

    lemma initial_threshold : 256 ≤ K 40000 := by
…

    Mentions: OAI.SmoothObstruction.WordParameters.K

  58. lemma OAI.SmoothObstruction.WordParameters.dimension_budget line 607

    Source documentation

    The actual nonzero symplectic sampler always has a nonzero choice.

    lemma dimension_budget {s : ℕ} (hK : 256 ≤ K s) : K s + 1 ≤ 2 * s := by
…

    Mentions: OAI.SmoothObstruction.WordParameters.K

  59. abbrev OAI.SmoothObstruction.WordAlphabet.Space line 631

    Source documentation

    The two coordinate halves of the source's F₂^(2s); this product is the canonical coordinate bijection, not a different graph or bilinear form.

    abbrev Space (s : ℕ) := (Fin s → ZMod 2) × (Fin s → ZMod 2)
  60. abbrev OAI.SmoothObstruction.WordAlphabet.Alphabet line 632
  61. def OAI.SmoothObstruction.WordAlphabet.form line 634
  62. lemma OAI.SmoothObstruction.WordAlphabet.form_apply line 645
  63. lemma OAI.SmoothObstruction.WordAlphabet.form_alt line 648
  64. lemma OAI.SmoothObstruction.WordAlphabet.form_symm line 656
  65. lemma OAI.SmoothObstruction.WordAlphabet.form_nondegenerate line 662
  66. lemma OAI.SmoothObstruction.WordAlphabet.finrank line 673
  67. lemma OAI.SmoothObstruction.WordAlphabet.card_space line 677
  68. lemma OAI.SmoothObstruction.WordAlphabet.card_alphabet line 683
  69. theorem OAI.SmoothObstruction.CheapScales.arbitrarily_late_cheap line 702

    Source documentation

    A summable nonnegative expense cannot dominate a nonsummable information budget on pairwise disjoint finite test sets.

    theorem arbitrarily_late_cheap {J : ℕ → Finset ℕ}
    (hJ : ∀ i i', i ≠ i' → Disjoint (J i) (J i'))
    {B R : ℕ → ℝ} (hR : ∀ i,0≤R i)
    (hBs : Summable (fun j => (B j)^16))
    (hRs : ¬Summable (fun i => (J i).card*(R i)^16))
    {ε : ℝ} (hε : 0<ε) (N : ℕ) :
    ∃ i≥N, ∃ j∈J i,B j<ε*R i := by
…
  70. theorem OAI.SmoothObstruction.CheapScales.cheap_sequence line 744

    Source documentation

    Successively late tests with ratios tending to zero; positivity is retained for the source information rate, so the ratio is not a totalized-division trick.

    theorem cheap_sequence {J : ℕ → Finset ℕ}
    (hJ : ∀ i i', i ≠ i' → Disjoint (J i) (J i'))
    {B R : ℕ → ℝ} (hB : ∀ j,0≤B j) (hR : ∀ i,0<R i)
    (hBs : Summable (fun j => (B j)^16))
    (hRs : ¬Summable (fun i => (J i).card*(R i)^16)) :
    ∃ (i j : ℕ → ℕ), (∀ a : ℕ, a ≤ i a) ∧ (∀ a : ℕ, j a ∈ J (i a)) ∧
      Tendsto i atTop atTop ∧ Tendsto (fun a => B (j a)/R (i a)) atTop (nhds 0) := by
…
  71. def OAI.SmoothObstruction.WordParameters.logLevel line 765
  72. def OAI.SmoothObstruction.WordParameters.testScales line 766
  73. lemma OAI.SmoothObstruction.WordParameters.logLevel_succ line 770
  74. lemma OAI.SmoothObstruction.WordParameters.logLevel_strictMono line 774
  75. lemma OAI.SmoothObstruction.WordParameters.testScales_disjoint line 781
  76. lemma OAI.SmoothObstruction.WordParameters.testScales_card line 796
  77. lemma OAI.SmoothObstruction.WordParameters.testScales_not_summable line 802
  78. theorem OAI.SmoothObstruction.WordParameters.actual_cheap_scales line 815

    Source documentation

    The source's actual disjoint tests, with their full stated range and no enlargement or alteration of the word recursion.

    theorem actual_cheap_scales {s₀ : ℕ} (h₀ : 256≤K s₀)
    {B : ℕ → ℝ} (hB : ∀ j,0<B j) (hBs : Summable (fun j => (B j)^16)) :
    ∃ (i j : ℕ → ℕ), (∀ a : ℕ,a≤ i a) ∧ (∀ a,j a∈testScales s₀ (i a)) ∧
      Tendsto i atTop atTop ∧
      Tendsto (fun a => B (j a)/rate s₀ (i a)) atTop (nhds 0) ∧
      ∀ a, ∃ t : ℕ, (K (sequence s₀ (i a))+15)/16≤t ∧
        t≤K (sequence s₀ (i a))/8 ∧
        length s₀ (i a)*2^t=2^(j a) ∧ 2≤2^t := by
…

    Mentions: OAI.SmoothObstruction.WordParameters.K, OAI.SmoothObstruction.WordParameters.testScales, OAI.SmoothObstruction.WordParameters.rate, OAI.SmoothObstruction.WordParameters.sequence, OAI.SmoothObstruction.WordParameters.length