OAI/Geometry/HarmonicGrowth/AngularStream.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicCounterexample.CausalConstruction.prefixes line 17

   Source documentation

   Prefixes contain genuine future zero controls, rather than the base point of an endpoint chart (whose control word need not vanish).

   def prefixes (zero : P) (choose : ℕ → (ℕ → P) → P) : ℕ → ℕ → P
     | 0 => fun _ => zero
     | n+1 => Function.update (prefixes zero choose n) n (choose n (prefixes zero choose n))

2. def OAI.HarmonicCounterexample.CausalConstruction.limitChoice line 21
3. lemma OAI.HarmonicCounterexample.CausalConstruction.prefixes_zero line 24
4. lemma OAI.HarmonicCounterexample.CausalConstruction.prefixes_stable line 32
5. theorem OAI.HarmonicCounterexample.CausalConstruction.causal_choice line 44

   Source documentation

   Pure dependent choice in chronological order. The predicate may depend on all past controls, but never on a fictitious future control.

   theorem causal_choice (zero : P) (admissible : Set P)
       (good : ℕ → (ℕ → P) → P → Prop)
       (produce : ∀ j s,(∀ i < j,s i ∈ admissible) → (∀ i,j ≤ i → s i=zero) →
         ∃ x ∈ admissible,good j s x) :
       ∃ s : ℕ → P,(∀ j,s j ∈ admissible) ∧
         ∀ j,good j (fun i => if i < j then s i else zero) (s j) := by
   …

6. theorem OAI.HarmonicCounterexample.CausalConstruction.smooth_escaping_sum line 85

   Source documentation

   Vector-valued local finiteness for the fixed polynomial schedule.

   theorem smooth_escaping_sum {f : ℕ → ℝ → E} (hf : ∀ j,ContDiff ℝ ∞ (f j))
       (hz : ∀ j t,t ≤ time j → f j t=0) :
       ContDiff ℝ ∞ (fun t => ∑' j,f j t) := by
   …

7. lemma OAI.HarmonicCounterexample.CausalConstruction.sum_period line 101

   Source documentation

   At every actual time in a period there is exactly one possible increment. Both endpoints have zero increments, so this holds on closed periods.

   lemma sum_period {f : ℕ → ℝ → E}
       (hz0 : ∀ j t,t ≤ time j → f j t=0)
       (hz1 : ∀ j t,time (j+1) ≤ t → f j t=0)
       {j : ℕ} {t : ℝ} (hlo : time j ≤ t) (hhi : t ≤ time (j+1)) :
       (∑' i,f i t)=f j t := by
   …

8. lemma OAI.HarmonicCounterexample.CausalConstruction.sum_initial line 113
9. lemma OAI.HarmonicCounterexample.CausalConstruction.sum_causal line 124

   Source documentation

   A future insertion cannot change a previous time, regardless of the infinite tail of controls. This is the causality needed by regular ODEs.

   lemma sum_causal {f g : ℕ → ℝ → E} {j : ℕ}
       (hf : ∀ i t,t ≤ time i → f i t=0)
       (hg : ∀ i t,t ≤ time i → g i t=0)
       (he : ∀ i < j,f i=g i) {t : ℝ} (ht : t ≤ time j) :
       (∑' i,f i t)=(∑' i,g i t) := by
   …

10. def OAI.HarmonicCounterexample.AngularStream.base line 149

    Source documentation

    The fixed diagonal leg; initially and during every pulse it is round.

    def base (qstar : ℝ) (j0 : ℕ) : ℝ → ℝ := Pulses.profile (fun _ _ => 0) qstar j0

    Mentions: OAI.HarmonicCounterexample.Pulses.profile

11. lemma OAI.HarmonicCounterexample.AngularStream.base_smooth line 151
12. lemma OAI.HarmonicCounterexample.AngularStream.base_initial line 154
13. lemma OAI.HarmonicCounterexample.AngularStream.base_pulse line 157
14. lemma OAI.HarmonicCounterexample.AngularStream.base_range line 162
15. def OAI.HarmonicCounterexample.AngularStream.increment line 172

    Source documentation

    Actual angular increment of a period, zero on both open round collars.

    def increment (r : ℝ) (b : E) (D : Fin n → E) (s : ℕ → Fin n → ℝ) (j : ℕ) (t : ℝ) : E :=
    …

    Mentions: OAI.HarmonicCounterexample.b

16. lemma OAI.HarmonicCounterexample.AngularStream.increment_before line 175
17. lemma OAI.HarmonicCounterexample.AngularStream.increment_after line 181
18. lemma OAI.HarmonicCounterexample.AngularStream.increment_zero line 189
19. def OAI.HarmonicCounterexample.AngularStream.activeIncrement line 195
20. lemma OAI.HarmonicCounterexample.AngularStream.active_before line 198
21. lemma OAI.HarmonicCounterexample.AngularStream.active_after line 204
22. def OAI.HarmonicCounterexample.AngularStream.angular line 214

    Source documentation

    Simultaneously smooth infinite angular coefficient. No angular selector is used in its definition, so discontinuous labels cannot spoil regularity.

    def angular (r : ℝ) (b D0 : E) (D : Fin n → E) (s : ℕ → Fin n → ℝ)
        (qstar : ℝ) (j0 : ℕ) (t : ℝ) : E :=
    …

    Mentions: OAI.HarmonicCounterexample.b

23. lemma OAI.HarmonicCounterexample.AngularStream.angular_smooth line 218
24. lemma OAI.HarmonicCounterexample.AngularStream.angular_initial line 236
25. lemma OAI.HarmonicCounterexample.AngularStream.angular_period line 246
26. lemma OAI.HarmonicCounterexample.AngularStream.angular_pulse line 254
27. lemma OAI.HarmonicCounterexample.AngularStream.angular_leg line 261
28. lemma OAI.HarmonicCounterexample.AngularStream.angular_causal line 267
29. lemma OAI.HarmonicCounterexample.AngularStream.active_summable line 290
30. lemma OAI.HarmonicCounterexample.AngularStream.angular_update line 300

    Source documentation

    Updating a previously zero pulse is exactly the actual smooth insertion, not merely equality of an ideal packet.

    lemma angular_update (r : ℝ) (b D0 : E) (D : Fin n → E) (s : ℕ → Fin n → ℝ)
        (x : Fin n → ℝ) (qstar : ℝ) {j0 j : ℕ} (hj : j0 ≤ j) (hz : s j=0) (t : ℝ) :
        angular r b D0 D (Function.update s j x) qstar j0 t=
          angular r b D0 D s qstar j0 t+
            (nonlinearBergerWord r b D x (pulse j) ((t-time j)/pulse j)-b) := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.AngularStream.angular

31. lemma OAI.HarmonicCounterexample.AngularStream.coefficient_update line 319
32. def OAI.HarmonicCounterexample.AngularStream.direction line 327
33. lemma OAI.HarmonicCounterexample.AngularStream.angular_representation line 331
34. theorem OAI.HarmonicCounterexample.AngularStream.angular_uniform_bound line 358

    Source documentation

    An actual all-time coefficient bound chosen before the entire sequence of controls and the starting index. Uniformity is compactness of one fixed angular family, not a bound on a posteriori chosen histories.

    theorem angular_uniform_bound [NeZero n] (r : ℝ) (b D0 : E) (D : Fin n → E)
        {qstar : ℝ} (hq : 1 ≤ qstar) :
        ∃ C : ℝ,0 ≤ C ∧ ∀ (s : ℕ → Fin n → ℝ) (j0 : ℕ),
          (∀ j,j0 ≤ j → ∀ t i,packetStretch (s j) (pulse j) t i ∈ Icc (1/2:ℝ) (3/2)) →
          ∀ t,‖angular r b D0 D s qstar j0 t‖ ≤ C := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.AngularStream.angular

35. lemma OAI.HarmonicCounterexample.AngularStream.angular_nonnegative line 393
36. lemma OAI.HarmonicCounterexample.AngularStream.angular_symmetric line 404
37. lemma OAI.HarmonicCounterexample.AngularStream.angular_zero_pulse line 418
38. lemma OAI.HarmonicCounterexample.AngularStream.angular_rest line 427

    Source documentation

    The preceding round rest is round even for the first active period, whose entire previous history is round. This uniformity is essential for recursion.

    lemma angular_rest (r : ℝ) (b D0 : E →L[ℝ] E) (D : Fin n → E →L[ℝ] E)
        (s : ℕ → Fin n → ℝ) {qstar t : ℝ} {j0 j : ℕ}
        (hlo : time j+3*pulse j+dwell j ≤ t) (hhi : t ≤ time (j+1)) :
        angular r b D0 D s qstar j0 t=b := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.AngularStream.angular