OAI/Geometry/HarmonicGrowth/Cycling.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicCounterexample.Cycling.partialSum line 11
2. lemma OAI.HarmonicCounterexample.Cycling.weighted_telescoping line 13
3. lemma OAI.HarmonicCounterexample.Cycling.weighted_sum_abs_le line 26

   Source documentation

   A bounded primitive makes every nonnegative monotone weighted mean asymptotically cancel at the scale of its largest weight.

   lemma weighted_sum_abs_le (f w : ℕ → ℝ) {C : ℝ} (hC : 0 ≤ C)
       (hpartial : ∀ n, |partialSum f n| ≤ C)
       (hw0 : 0 ≤ w 0) (hw : Monotone w) (n : ℕ) :
       |∑ j ∈ Finset.range n, w j * f j| ≤ 2 * C * w n := by
   …

   Mentions: OAI.HarmonicCounterexample.Cycling.partialSum

4. lemma OAI.HarmonicCounterexample.Cycling.partialSum_periodic line 49
5. lemma OAI.HarmonicCounterexample.Cycling.bounded_primitive_of_periodic line 60

   Source documentation

   Full cycles cancel exactly; only a bounded incomplete cycle remains.

   lemma bounded_primitive_of_periodic (f : ℕ → ℝ) {M : ℕ} (hM : 0 < M)
       (hper : Function.Periodic f M) (hzero : partialSum f M = 0) :
       ∀ n, |partialSum f n| ≤ ∑ j ∈ Finset.range M, |f j| := by
   …

   Mentions: OAI.HarmonicCounterexample.Cycling.partialSum

6. lemma OAI.HarmonicCounterexample.Cycling.weighted_periodic_abs_le line 71
7. theorem OAI.HarmonicCounterexample.Cycling.weighted_periodic_limit line 81

   Source documentation

   The precise asymptotic cancellation required by the cycling argument. No assumption of equal durations is made.

   theorem weighted_periodic_limit (f w D : ℕ → ℝ) {M : ℕ} (hM : 0 < M)
       (hper : Function.Periodic f M) (hzero : partialSum f M = 0)
       (hw0 : 0 ≤ w 0) (hw : Monotone w) (hD : ∀ n, 0 < D n)
       (hsmall : Tendsto (fun n => w n / D n) atTop (𝓝 0)) :
       Tendsto (fun n => (∑ j ∈ Finset.range n, w j * f j) / D n)
         atTop (𝓝 0) := by
   …

   Mentions: OAI.HarmonicCounterexample.Cycling.partialSum

8. lemma OAI.HarmonicCounterexample.Cycling.pulse_little_dwell line 108
9. lemma OAI.HarmonicCounterexample.Cycling.dwellSum_big_time line 122
10. lemma OAI.HarmonicCounterexample.Cycling.small_weighted_error line 133
11. lemma OAI.HarmonicCounterexample.Cycling.small_sum_time line 141
12. theorem OAI.HarmonicCounterexample.Cycling.endpoint_rate line 149

    Source documentation

    The full endpoint growth calculation: unequal j^7 dwell lengths, O(j^6) scalar factors, and uniformly vanishing exponent errors are all retained.

    theorem endpoint_rate {M : ℕ} (hM : 0 < M) (d scalarError exponentError : ℕ → ℝ)
        (hper : Function.Periodic d M) (average : ℝ)
        (haverage : (∑ j ∈ Finset.range M, d j) = (M : ℝ) * average)
        {C : ℝ} (hscalar : ∀ᶠ j in atTop, |scalarError j| ≤ C * pulse j)
        (hexponent : Tendsto exponentError atTop (𝓝 0)) :
        Tendsto (fun n => (∑ j ∈ Finset.range n,
          (scalarError j + dwell j * (d j + exponentError j))) / time n)
          atTop (𝓝 average) := by
    …

13. theorem OAI.HarmonicCounterexample.Cycling.remove_initial_history line 191

    Source documentation

    Ignoring a fixed initial history does not change the endpoint exponent.

    theorem remove_initial_history {f : ℕ → ℝ} {average : ℝ}
        (hf : Tendsto (fun n => (∑ j ∈ Finset.range n, f j) / time n)
          atTop (𝓝 average)) (j₀ : ℕ) :
        Tendsto (fun n => (∑ j ∈ Finset.Ico j₀ n, f j) / time n)
          atTop (𝓝 average) := by
    …

14. def OAI.HarmonicCounterexample.Cycling.transferOrbit line 221

    Source documentation

    Actual chronological product of endpoint transmission operators.

    def transferOrbit (T : ℕ → E →L[ℝ] E) (x : E) : ℕ → E
      | 0 => x
      | n+1 => T n (transferOrbit T x n)
    
    /-- The signed amplitudes retain all determinant-correcting signs. -/

15. def OAI.HarmonicCounterexample.Cycling.orbitAmplitude line 226

    Source documentation

    The signed amplitudes retain all determinant-correcting signs.

    def orbitAmplitude (π : Equiv.Perm ι) (σ : ι → ℝ) (s : ℕ → ℝ)
        (d : ℕ → ι → ℝ) (i : ι) (n : ℕ) : ℝ :=
    …

16. lemma OAI.HarmonicCounterexample.Cycling.transferOrbit_eq_signed_basis line 231
17. lemma OAI.HarmonicCounterexample.Cycling.orbitAmplitude_abs line 244
18. theorem OAI.HarmonicCounterexample.Cycling.signed_cycle_log_norm line 254

    Source documentation

    The exact source cycle-sum formula for true operator products. This also proves nonvanishing, so taking the real logarithm introduces no zero case.

    theorem signed_cycle_log_norm (b : ι → E) (hb : ∀ i,‖b i‖=1)
        (π : Equiv.Perm ι) (σ : ι → ℝ) (s : ℕ → ℝ) (d : ℕ → ι → ℝ)
        (T : ℕ → E →L[ℝ] E)
        (hT : ∀ n i,T n (b i)=(s n*σ i*d n i) • b (π i))
        (hσ : ∀ i,|σ i|=1) (hs : ∀ n,0<s n) (hd : ∀ n i,0<d n i)
        (i : ι) (n : ℕ) :
        0<‖transferOrbit T (b i) n‖ ∧
          Real.log ‖transferOrbit T (b i) n‖=
            ∑ j ∈ Finset.range n,(Real.log (s j)+Real.log (d j ((π^[j]) i))) := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.Cycling.transferOrbit

19. def OAI.HarmonicCounterexample.Cycling.signedPermutation line 275

    Source documentation

    A determinant-one signed permutation with the requested underlying cycle. One sign correction at i0 is enough and does not alter any coordinate norm.

    def signedPermutation (π : Equiv.Perm ι) (i₀ : ι) : Matrix ι ι ℝ :=
    …

20. lemma OAI.HarmonicCounterexample.Cycling.signedPermutation_det line 278
21. lemma OAI.HarmonicCounterexample.Cycling.finRotate_iterate_add line 285
22. lemma OAI.HarmonicCounterexample.Cycling.cycle_exponents_periodic line 294
23. lemma OAI.HarmonicCounterexample.Cycling.cycle_exponents_sum line 299
24. lemma OAI.HarmonicCounterexample.Cycling.signedPermutation_mulVec_single line 306
25. lemma OAI.HarmonicCounterexample.Cycling.signedPermutation_abs_sign line 316
26. lemma OAI.HarmonicCounterexample.Cycling.finite_varying_error line 335
27. theorem OAI.HarmonicCounterexample.Cycling.endpoint_operator_rate line 346

    Source documentation

    True endpoint operators, including the determinant-correcting signs and all scalar-normalization factors, have the averaged selected exponent. This is not an endpoint-only definition of polynomial growth.

    theorem endpoint_operator_rate {M : ℕ} [NeZero M] (b : Fin M → E)
        (hb : ∀ i,‖b i‖=1) (σ : Fin M → ℝ) (s : ℕ → ℝ)
        (d : ℕ → Fin M → ℝ) (T : ℕ → E →L[ℝ] E)
        (hT : ∀ n i,T n (b i)=(s n*σ i*d n i) • b (finRotate M i))
        (hσ : ∀ i,|σ i|=1) (hs : ∀ n,0<s n) (hd : ∀ n i,0<d n i)
        (d₀ : Fin M → ℝ) (e : ℕ → Fin M → ℝ)
        (hlog : ∀ n i,Real.log (d n i)=dwell n*(d₀ i+e n i))
        (he : ∀ i,Tendsto (fun n => e n i) atTop (𝓝 0))
        {C : ℝ} (hscalar : ∀ᶠ n in atTop,|Real.log (s n)| ≤ C*pulse n)
        (i : Fin M) :
        Tendsto (fun n => Real.log ‖transferOrbit T (b i) n‖ / time n)
          atTop (𝓝 ((∑ k,d₀ k)/(M:ℝ))) := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.Cycling.transferOrbit

28. def OAI.HarmonicCounterexample.Cycling.fromMatrix line 386
29. lemma OAI.HarmonicCounterexample.Cycling.fromMatrix_matrix line 389
30. lemma OAI.HarmonicCounterexample.Cycling.fromMatrix_inverse line 394
31. lemma OAI.HarmonicCounterexample.Cycling.basis_repr_fun line 400
32. def OAI.HarmonicCounterexample.Cycling.weightedCycle line 405
33. lemma OAI.HarmonicCounterexample.Cycling.weightedCycle_action line 409
34. lemma OAI.HarmonicCounterexample.Cycling.weightedCycle_injective line 426
35. lemma OAI.HarmonicCounterexample.Cycling.transferOrbit_linear line 446
36. lemma OAI.HarmonicCounterexample.Cycling.transferOrbit_injective line 454
37. lemma OAI.HarmonicCounterexample.AngularStream.pulse_unique line 471
38. def OAI.HarmonicCounterexample.AngularStream.pulseIndex line 483
39. lemma OAI.HarmonicCounterexample.AngularStream.pulseIndex_some line 487
40. lemma OAI.HarmonicCounterexample.AngularStream.pulseIndex_spec line 495
41. lemma OAI.HarmonicCounterexample.AngularStream.pulseIndex_none_iff line 502
42. lemma OAI.HarmonicCounterexample.AngularStream.pulseIndex_local_none line 515

    Source documentation

    The union of the physical closed pulse intervals is locally finite.

    lemma pulseIndex_local_none {j0 : ℕ} {t : ℝ} (h : pulseIndex j0 t=none) :
        ∀ᶠ u in 𝓝 t,pulseIndex j0 u=none := by
    …

    Mentions: OAI.HarmonicCounterexample.AngularStream.pulseIndex

43. lemma OAI.HarmonicCounterexample.AngularStream.pulseIndex_local_some line 533
44. def OAI.HarmonicCounterexample.AngularStream.globalSlot line 542

    Source documentation

    One angular choice for the ENTIRE infinite history. At all diagonal legs it is the distinguished background choice none.

    def globalSlot (d : ℝ → Fin n) (j0 : ℕ) (t : ℝ) : Option (Fin n) :=
    …

45. lemma OAI.HarmonicCounterexample.AngularStream.globalSlot_local_or_round line 547
46. lemma OAI.HarmonicCounterexample.AngularStream.angular_globalSlot line 576

    Source documentation

    Exact identification of the constructed angular stream with the genuine Berger scalar/operator model for that SAME single global selector.

    lemma angular_globalSlot (r : ℝ) (b D₀ : E) (D : Fin n → E)
        (d : ℝ → Fin n) (hd : ∀ t i,i ≠ d t → bump i (duration n*t)=0)
        (s : ℕ → Fin n → ℝ) (qstar : ℝ) (j0 : ℕ) (t : ℝ) :
        angular r b D₀ D s qstar j0 t=
          PulseTaylor.angular r b ((globalSlot d j0 t).elim D₀ D) (scalar s qstar j0 t) := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.AngularStream.angular, OAI.HarmonicCounterexample.PulseTaylor.angular, OAI.HarmonicCounterexample.AngularStream.globalSlot, OAI.HarmonicCounterexample.AngularStream.scalar