OAI/Dynamics/ThreeTorus/PredictionModels.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

Block tests, diagonal predictions, centering, and stability of finite-color models.

  1. lemma OAI.ThreeTorus.PhaseLaurent.coordinate line 16
  2. lemma OAI.ThreeTorus.PhaseLaurent.blockFactor line 21
  3. lemma OAI.ThreeTorus.PhaseLaurent.blockProduct line 31
  4. lemma OAI.ThreeTorus.CircleBounded.neg line 37
  5. lemma OAI.ThreeTorus.CircleBounded.sub line 41
  6. lemma OAI.ThreeTorus.circleBounded_ofReal line 45
  7. def OAI.ThreeTorus.blockTotal line 52
  8. def OAI.ThreeTorus.blockWeights line 55
  9. def OAI.ThreeTorus.blockTagMean line 58
  10. lemma OAI.ThreeTorus.blockTotal_nonneg line 61
  11. lemma OAI.ThreeTorus.continuous_blockTotal line 65
  12. lemma OAI.ThreeTorus.blockWeights_bounds line 69
  13. lemma OAI.ThreeTorus.sum_blockWeights line 80
  14. lemma OAI.ThreeTorus.circleBounded_blockWeights line 85
  15. def OAI.ThreeTorus.blockSqrtTest line 96

    Source documentation

    The exact polynomial lower bound, not the non-polynomial square root.

    def blockSqrtTest {m : ℕ} (p : Fin m → UnitAddCircle → ℝ) (b : Fin m → ℂ)
    (q : UnitAddCircle → ℂ) (n : ℕ) (ell : ℝ)
    (z : UnitAddCircle) (y : Fin n → UnitAddCircle) : ℝ :=
…
  16. def OAI.ThreeTorus.blockPhaseEstimator line 102
  17. def OAI.ThreeTorus.blockErrorTest line 106
  18. lemma OAI.ThreeTorus.phaseLaurent_blockMixture line 112
  19. lemma OAI.ThreeTorus.phaseLaurent_blockSqrtTest line 122
  20. lemma OAI.ThreeTorus.phaseLaurent_blockPhaseEstimator line 139
  21. lemma OAI.ThreeTorus.phaseLaurent_blockErrorTest line 145
  22. lemma OAI.ThreeTorus.CircleBounded.sum line 170
  23. lemma OAI.ThreeTorus.PhaseLaurent.diagonal_bounded line 181
  24. lemma OAI.ThreeTorus.integral_phaseTest_pointwise line 193
  25. lemma OAI.ThreeTorus.PhaseLaurent.independent_bounded line 212
  26. lemma OAI.ThreeTorus.PhaseLaurent.diagonal_integrable_real line 226
  27. lemma OAI.ThreeTorus.PhaseLaurent.independent_integrable_real line 232
  28. lemma OAI.ThreeTorus.blockMixture_polynomial_integral line 238
  29. lemma OAI.ThreeTorus.blockTagMean_centered line 257
  30. lemma OAI.ThreeTorus.blockSqrtTest_independent_bound line 267
  31. lemma OAI.ThreeTorus.blockPhaseEstimator_noise line 286
  32. lemma OAI.ThreeTorus.blockErrorTest_independent_exact line 297
  33. lemma OAI.ThreeTorus.CircleBounded.norm_sq line 322
  34. lemma OAI.ThreeTorus.integrable_real_of_circleBounded line 326
  35. lemma OAI.ThreeTorus.circleBounded_blockTagMean line 330
  36. lemma OAI.ThreeTorus.integral_sqrt_le_sqrt_two line 336
  37. lemma OAI.ThreeTorus.blockSqrtTest_integral_bound line 361
  38. def OAI.ThreeTorus.blockPreviousError line 396
  39. lemma OAI.ThreeTorus.integrable_blockPreviousError line 400
  40. lemma OAI.ThreeTorus.blockErrorTest_integral_bound line 409
  41. def OAI.ThreeTorus.blockModelDensity line 453
  42. lemma OAI.ThreeTorus.blockTotal_mul_blockWeights line 458
  43. lemma OAI.ThreeTorus.blockModelDensity_eq line 469
  44. lemma OAI.ThreeTorus.blockModelDensity_nonneg line 479
  45. lemma OAI.ThreeTorus.blockSqrtTest_le_model_sqrt line 489
  46. lemma OAI.ThreeTorus.continuous_blockModel_diagonal line 500
  47. theorem OAI.ThreeTorus.block_model_diagonal line 510

    Source documentation

    The exact Hellinger and previous-estimator estimates of source 04 on one common actual diagonal, with arbitrary successive geometric lower bounds. This is the analytic model step, not the geometric prediction proposition.

    theorem block_model_diagonal {m n : ℕ} {p : Fin m → UnitAddCircle → ℝ}
    (hp : ∀ r z, 0 ≤ p r z) (hc : ∀ r, Continuous (p r)) (b : Fin m → ℂ)
    (hb : ∀ r, ‖b r‖ ≤ 1) {q A : UnitAddCircle → ℂ} (hq : Continuous q)
    (hqB : ∀ z, ‖q z‖ ≤ 2) (hA : CircleBounded A) (k : ℕ)
    {ell delta eta : ℝ} (hell : 0 < ell) (hs : 6*ell ≤ 1)
    (hd : 0 < delta) (hd1 : delta ≤ 1/100)
    (hn0 : delta/2 ≤ (n:ℝ)*ell^2) (hn1 : (n:ℝ)*ell^2 ≤ delta)
    (hmass : (∫ z, blockTotal p z ∂phaseHaar) ≤ 2)
    (hcenter : (∫ z, Real.sqrt (blockTotal p z)*‖blockTagMean p b z-q z‖^2 ∂phaseHaar) ≤ delta)
    (heta : 0 < eta) (B : (j : ℕ) → (Fin j → ℤ) → ℤ) :
    ∃ L : Fin n → ℤ, (∀ j, 0 < L j) ∧
      (∀ j : Fin n, B j (fun i => L ⟨i.val, i.isLt.trans j.isLt⟩) < L j) ∧
…

    Mentions: OAI.ThreeTorus.CircleBounded, OAI.ThreeTorus.blockTotal, OAI.ThreeTorus.phaseHaar, OAI.ThreeTorus.blockTagMean

  48. def OAI.ThreeTorus.blockNumerator line 577
  49. def OAI.ThreeTorus.blockCenter line 580
  50. lemma OAI.ThreeTorus.blockNumerator_norm line 584
  51. lemma OAI.ThreeTorus.blockTagMean_eq line 594
  52. lemma OAI.ThreeTorus.blockTagMean_norm line 600
  53. lemma OAI.ThreeTorus.blockCenter_norm line 610
  54. lemma OAI.ThreeTorus.blockCenter_error_eq line 620
  55. lemma OAI.ThreeTorus.blockCenter_error_bound line 643
  56. lemma OAI.ThreeTorus.sqrt_weighted_regularization_bound line 652
  57. lemma OAI.ThreeTorus.continuous_blockNumerator line 671
  58. lemma OAI.ThreeTorus.continuous_blockCenter line 676
  59. lemma OAI.ThreeTorus.blockCenter_integral_error line 686
  60. lemma OAI.ThreeTorus.exists_block_center line 705
  61. lemma OAI.ThreeTorus.contDiff_blockCenter_lift line 719

    Source documentation

    The regularized center is genuinely smooth as a circle function whenever its finite color densities are smooth; no regularity of beta is needed at zeros.

    lemma contDiff_blockCenter_lift {m : ℕ} {p : Fin m → UnitAddCircle → ℝ}
    (hp : ∀ r z, 0 ≤ p r z)
    (hs : ∀ r, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (fun x : ℝ => p r (x : UnitAddCircle)))
    (b : Fin m → ℂ) {epsilon : ℝ} (he : 0 < epsilon) :
    ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
      (fun x : ℝ => blockCenter p b epsilon (x : UnitAddCircle)) := by
…

    Mentions: OAI.ThreeTorus.blockCenter

  62. lemma OAI.ThreeTorus.blockTotal_reflection line 739
  63. lemma OAI.ThreeTorus.blockNumerator_reflection line 746
  64. lemma OAI.ThreeTorus.blockCenter_reflection line 754
  65. theorem OAI.ThreeTorus.exists_smooth_symmetric_block_center line 764

    Source documentation

    Source 04 centering with its smoothness, norm, and conjugation requirements. The explicit center even has norm at most one (the source permits two).

    theorem exists_smooth_symmetric_block_center {m : ℕ}
    {p : Fin m → UnitAddCircle → ℝ} (hp : ∀ r z, 0 ≤ p r z)
    (hc : ∀ r, Continuous (p r))
    (hs : ∀ r, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (fun x : ℝ => p r (x : UnitAddCircle)))
    {b : Fin m → ℂ} (hb : ∀ r, ‖b r‖ ≤ 1) (e : Equiv.Perm (Fin m))
    (hpr : ∀ r z, p (e r) (-z) = p r z) (hbr : ∀ r, b (e r) = conj (b r))
    {delta : ℝ} (hd : 0 < delta) :
    ∃ q : UnitAddCircle → ℂ, Continuous q ∧
      ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (fun x : ℝ => q (x : UnitAddCircle)) ∧
      (∀ z, ‖q z‖ ≤ 2) ∧ (∀ z, q (-z) = conj (q z)) ∧
      (∫ z, Real.sqrt (blockTotal p z)*‖blockTagMean p b z-q z‖^2 ∂phaseHaar) < delta := by
…

    Mentions: OAI.ThreeTorus.blockTotal, OAI.ThreeTorus.blockTagMean, OAI.ThreeTorus.phaseHaar

  66. def OAI.ThreeTorus.colorL1Distance line 798
  67. lemma OAI.ThreeTorus.colorL1Distance_nonneg line 801
  68. lemma OAI.ThreeTorus.continuous_circle_integrable line 805
  69. lemma OAI.ThreeTorus.integral_sqrt_le_sqrt_integral line 809
  70. lemma OAI.ThreeTorus.sqrt_le_sqrt_add_sqrt_error line 832
  71. theorem OAI.ThreeTorus.color_hellinger_stability line 843

    Source documentation

    Total Hellinger loss is bounded by the square root of total color L1 loss.

    theorem color_hellinger_stability {m : ℕ} {p g : Fin m → UnitAddCircle → ℝ}
    (hp : ∀ r z, 0 ≤ p r z) (hg : ∀ r z, 0 ≤ g r z)
    (hcp : ∀ r, Continuous (p r)) (hcg : ∀ r, Continuous (g r)) :
    (∫ z, Real.sqrt (blockTotal p z) ∂phaseHaar) ≤
      (∫ z, Real.sqrt (blockTotal g z) ∂phaseHaar)+Real.sqrt (colorL1Distance p g) := by
…

    Mentions: OAI.ThreeTorus.blockTotal, OAI.ThreeTorus.phaseHaar, OAI.ThreeTorus.colorL1Distance

  72. theorem OAI.ThreeTorus.color_weighted_stability line 871

    Source documentation

    Bounded weights transfer the model prediction integral to actual densities.

    theorem color_weighted_stability {m : ℕ} {p g w : Fin m → UnitAddCircle → ℝ}
    (hcp : ∀ r, Continuous (p r)) (hcg : ∀ r, Continuous (g r))
    (hcw : ∀ r, Continuous (w r)) {W : ℝ}
    (hw : ∀ r z, 0 ≤ w r z ∧ w r z ≤ W) :
    (∑ r, ∫ z, g r z*w r z ∂phaseHaar) ≤
      (∑ r, ∫ z, p r z*w r z ∂phaseHaar)+W*colorL1Distance p g := by
…

    Mentions: OAI.ThreeTorus.phaseHaar, OAI.ThreeTorus.colorL1Distance

  73. lemma OAI.ThreeTorus.colorL1Distance_triangle line 896
  74. lemma OAI.ThreeTorus.colorL1Distance_mul_bound line 911
  75. lemma OAI.ThreeTorus.finite_error_propagation line 932

    Source documentation

    The geometric amplification is finite and fixed before choosing any anchor accuracy, even when the block length is very large.

    lemma finite_error_propagation {E : ℕ → ℝ} {M t : ℝ} (hM : 1 ≤ M) (ht : 0 ≤ t)
    (h0 : E 0 ≤ t) (hstep : ∀ i, E (i+1) ≤ M*E i+t) (n : ℕ) :
    E n ≤ ((n:ℝ)+1)*M^n*t := by
…