StreamData.lean`

103 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HarmonicCounterexample.AngularStream.scalarPacket_smooth line 16
lemma OAI.HarmonicCounterexample.AngularStream.scalarPacket_before line 21
lemma OAI.HarmonicCounterexample.AngularStream.scalarPacket_after line 29
lemma OAI.HarmonicCounterexample.AngularStream.scalarPacket_zero_before line 38
lemma OAI.HarmonicCounterexample.AngularStream.scalarPacket_zero_after line 41
def OAI.HarmonicCounterexample.AngularStream.scalar line 47
Source documentation
The ONE genuine smooth scalar anisotropy attached to an infinite stream.
```
def scalar (s : ℕ → Fin n → ℝ) (qstar : ℝ) (j0 : ℕ) : ℝ → ℝ :=
…
```
lemma OAI.HarmonicCounterexample.AngularStream.scalar_smooth line 50
lemma OAI.HarmonicCounterexample.AngularStream.scalar_initial line 53
lemma OAI.HarmonicCounterexample.AngularStream.scalar_pulse line 56
lemma OAI.HarmonicCounterexample.AngularStream.scalar_leg line 62
lemma OAI.HarmonicCounterexample.AngularStream.scalar_rest line 70
lemma OAI.HarmonicCounterexample.AngularStream.scalar_start_collar line 76
Source documentation
Open round collar at the START of every pulse, including the FIRST one.
```
lemma scalar_start_collar (s : ℕ → Fin n → ℝ) (qstar : ℝ) {j0 j : ℕ} (hj : j0 ≤ j) :
    ∀ᶠ t in 𝓝 (time j),scalar s qstar j0 t=1 := by
…
```
Mentions: OAI.HarmonicCounterexample.AngularStream.scalar
lemma OAI.HarmonicCounterexample.AngularStream.scalar_end_collar line 97
Source documentation
Open round collar at the END of every pulse. The next ramp starts only AFTER this collar, so changing back to the dwell angular structure is smooth.
```
lemma scalar_end_collar (s : ℕ → Fin n → ℝ) (qstar : ℝ) {j0 j : ℕ} (hj : j0 ≤ j) :
    ∀ᶠ t in 𝓝 (time j+pulse j),scalar s qstar j0 t=1 := by
…
```
Mentions: OAI.HarmonicCounterexample.AngularStream.scalar
def OAI.HarmonicCounterexample.AngularStream.scalarShape line 125
lemma OAI.HarmonicCounterexample.AngularStream.scalarShape_smooth line 127
lemma OAI.HarmonicCounterexample.AngularStream.scalarShape_local_zero line 130
lemma OAI.HarmonicCounterexample.AngularStream.scalarShape_two_bound line 145
lemma OAI.HarmonicCounterexample.AngularStream.scalarPacket_as_sum line 154
lemma OAI.HarmonicCounterexample.AngularStream.scalarPacket_deriv line 160
lemma OAI.HarmonicCounterexample.AngularStream.scalarPacket_deriv_two line 166
theorem OAI.HarmonicCounterexample.AngularStream.scalarPacket_two_uniform_bound line 174
Source documentation
The second time jet is uniformly bounded on the same fixed amplitude box. This constant is chosen before the entire infinite history.
```
theorem scalarPacket_two_uniform_bound (n : ℕ) : ∃ C : ℝ,0 ≤ C ∧
    ∀ (a : Fin n → ℝ) (M : ℝ),0 ≤ M → (∀ i,|a i| ≤ M) →
      ∀ t,|deriv (deriv (unitPacketScalar a)) t| ≤ C*M := by
…
```
Mentions: OAI.HarmonicCounterexample.a
lemma OAI.HarmonicCounterexample.AngularStream.scalarPacket_deriv_eq line 188

theorem OAI.HarmonicCounterexample.LinearODE.PhysicalWord.scalar_uniform_bounds line 210

Source documentation

All three profile jet constants are selected before histories.

theorem PhysicalWord.scalar_uniform_bounds : ∃ M C1 C2 : ℝ,
    0 ≤ M ∧ 0 ≤ C1 ∧ 0 ≤ C2 ∧
    ∀ s : ℕ → Fin w.n → ℝ,(∀ j,s j ∈ w.admissible) → ∀ j t,
      |unitPacketScalar (s j) t| ≤ M ∧
      |deriv (unitPacketScalar (s j)) t| ≤ C1 ∧
      |deriv (deriv (unitPacketScalar (s j))) t| ≤ C2 := by
…

theorem OAI.HarmonicCounterexample.LinearODE.PhysicalWord.profile_uniform_bounds line 237

Source documentation

The complete global profile has uniform jet budgets selected before every history and before the late starting index.

theorem PhysicalWord.profile_uniform_bounds (qstar : ℝ) : ∃ M C1 C2 : ℝ,
    0 ≤ M ∧ 0 ≤ C1 ∧ 0 ≤ C2 ∧
    ∀ s : ℕ → Fin w.n → ℝ,(∀ j,s j ∈ w.admissible) →
      (∀ j t,|unitPacketScalar (s j) t| ≤ M) ∧
      ∀ j0 j,j0 ≤ j → ∀ t ∈ Icc (time j) (time (j+1)),
        |deriv (scalar s qstar j0) t| ≤ C1/pulse j ∧
        |deriv (deriv (scalar s qstar j0)) t| ≤ C2/pulse j^2 := by
…

lemma OAI.HarmonicCounterexample.LinearODE.PhysicalWord.scalar_positive_threshold line 260

theorem OAI.HarmonicCounterexample.LinearODE.PhysicalWord.curvature_threshold line 278

Source documentation

One geometric threshold, before the subsequently tuned infinite stream, absorbs the radial and BOTH tangent curvature costs on EVERY active period.

theorem PhysicalWord.curvature_threshold {m a μ qstar : ℝ}
    (hm : 1 ≤ m) (hμ : 0 < μ) (hμ1 : μ ≤ 1/4) (hqstar : 1 ≤ qstar)
    (ha : Tendsto (Scale.profile μ) atTop (𝓝 a))
    (hH : ∀ q ∈ Icc 1 qstar,0 < m+1-2*q-(m-1)*a^2*q^(-1/m))
    (hV : ∀ q ∈ Icc 1 qstar,0 < (m-1)*q*(q-a^2*q^(-1/m))) :
    ∃ J : ℕ,∀ j0,J ≤ j0 → ∀ s : ℕ → Fin w.n → ℝ,
      (∀ j,s j ∈ w.admissible) →
      (∀ t,1/2 ≤ scalar s qstar j0 t ∧ scalar s qstar j0 t ≤ qstar+1/2) ∧
      ∀ j,j0 ≤ j → ∀ t ∈ Icc (time j) (time (j+1)),
        let q := scalar s qstar j0
…

Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.Scale.profile

lemma OAI.HarmonicCounterexample.Berger.static_horizontal_margin line 325
Source documentation
The horizontal Ricci margin is smallest at the Berger dwell endpoint, not at an untested point of the ramp.
```
lemma static_horizontal_margin {m a q qstar : ℝ} (hm : 1 < m) (ha : a^2 < 1)
    (hq : q ∈ Set.Icc 1 qstar)
    (hstar : 0 < m+1-2*qstar-(m-1)*a^2*qstar^(-1/m)) :
    0 < m+1-2*q-(m-1)*a^2*q^(-1/m) := by
…
```
Mentions: OAI.HarmonicCounterexample.a
def OAI.HarmonicCounterexample.Construction.qstar line 367
def OAI.HarmonicCounterexample.Construction.a line 369
lemma OAI.HarmonicCounterexample.Construction.qstar_pos line 371
lemma OAI.HarmonicCounterexample.Construction.qstar_ge_one line 372
lemma OAI.HarmonicCounterexample.Construction.a_pos line 373
lemma OAI.HarmonicCounterexample.Construction.a_square line 374
lemma OAI.HarmonicCounterexample.Construction.qstar_small_power line 377
lemma OAI.HarmonicCounterexample.Construction.a_square_lt_one line 384
lemma OAI.HarmonicCounterexample.Construction.a_lt_one line 389
lemma OAI.HarmonicCounterexample.Construction.a_lower line 391
lemma OAI.HarmonicCounterexample.Construction.scale_total_lower line 396
lemma OAI.HarmonicCounterexample.Construction.a_close line 403
lemma OAI.HarmonicCounterexample.Construction.static_horizontal line 411
lemma OAI.HarmonicCounterexample.Construction.static_vertical line 423
lemma OAI.HarmonicCounterexample.Construction.exists_scale line 427
lemma OAI.HarmonicCounterexample.Control.conj_traceFree line 444
lemma OAI.HarmonicCounterexample.Control.conj_mul line 450
lemma OAI.HarmonicCounterexample.Control.complexify_one line 456
lemma OAI.HarmonicCounterexample.Control.complexify_traceFree line 461
lemma OAI.HarmonicCounterexample.Control.restrictReal_traceFree_square line 473
lemma OAI.HarmonicCounterexample.Control.cartesian_conj_rotation line 485
def OAI.HarmonicCounterexample.Control.cartesianGenerator line 493
Source documentation
Actual Cartesian generators share the original real-form simultaneous control.
```
def cartesianGenerator (L:ℕ) (c:Fin L→ℝ) (J:ComplexStructure (Fin 8⊕Fin 8)) :
    ∀l:Fin L,Module.End ℝ (Angular.harmonicPolynomials 16 (l.val+2)) := fun l=>
…
```
Mentions: OAI.HarmonicCounterexample.Angular.harmonicPolynomials
def OAI.HarmonicCounterexample.Control.endTupleConj line 498
def OAI.HarmonicCounterexample.Control.cartesianTupleEquiv line 504
lemma OAI.HarmonicCounterexample.Control.cartesianTupleEquiv_apply line 509
lemma OAI.HarmonicCounterexample.Control.cartesian_generator_eq line 513
theorem OAI.HarmonicCounterexample.Control.cartesian_simultaneous line 522
def OAI.HarmonicCounterexample.Control.matrixTupleEquiv line 554
lemma OAI.HarmonicCounterexample.Control.matrixTupleEquiv_apply line 558
theorem OAI.HarmonicCounterexample.Control.simultaneous_toMatrix line 561
lemma OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix_eigen line 587
structure OAI.HarmonicCounterexample.LinearODE.SpectralData line 591
def OAI.HarmonicCounterexample.LinearODE.spectralData line 597
abbrev OAI.HarmonicCounterexample.Construction.H line 613
abbrev OAI.HarmonicCounterexample.Construction.Index line 614
abbrev OAI.HarmonicCounterexample.Construction.CS line 615
def OAI.HarmonicCounterexample.Construction.Jround line 616
def OAI.HarmonicCounterexample.Construction.D line 618
def OAI.HarmonicCounterexample.Construction.Dround line 621
lemma OAI.HarmonicCounterexample.Construction.dim_ge_two line 623
instance OAI.HarmonicCounterexample.Construction.indexNontrivial line 630
instance OAI.HarmonicCounterexample.Construction.CSnonempty line 631
lemma OAI.HarmonicCounterexample.Construction.D_symmetric line 633
lemma OAI.HarmonicCounterexample.Construction.Dround_symmetric line 636
def OAI.HarmonicCounterexample.Construction.spectrum line 638
abbrev OAI.HarmonicCounterexample.Construction.basis line 639
abbrev OAI.HarmonicCounterexample.Construction.d0 line 640
lemma OAI.HarmonicCounterexample.Construction.basis_eigen line 642
lemma OAI.HarmonicCounterexample.Construction.Dround_diagonal line 645
def OAI.HarmonicCounterexample.Construction.degree line 648
def OAI.HarmonicCounterexample.Construction.B line 649
def OAI.HarmonicCounterexample.Construction.beta line 650
def OAI.HarmonicCounterexample.Construction.theta line 651
lemma OAI.HarmonicCounterexample.Construction.degree_pos line 653
lemma OAI.HarmonicCounterexample.Construction.B_pos line 654
lemma OAI.HarmonicCounterexample.Construction.beta_pos line 655
lemma OAI.HarmonicCounterexample.Construction.theta_pos line 656
lemma OAI.HarmonicCounterexample.Construction.theta_root line 661
lemma OAI.HarmonicCounterexample.Construction.D_nonpos line 665
lemma OAI.HarmonicCounterexample.Construction.D_lower line 669
def OAI.HarmonicCounterexample.Construction.system line 676
lemma OAI.HarmonicCounterexample.LinearODE.slow_linearMap line 704
lemma OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix_eq_matrix line 711
lemma OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix_toMatrix line 718
lemma OAI.HarmonicCounterexample.Control.matrixTupleEquiv_trace line 734
lemma OAI.HarmonicCounterexample.Construction.D_trace line 750
lemma OAI.HarmonicCounterexample.Construction.rank_ne line 756
lemma OAI.HarmonicCounterexample.Construction.traceFree_D line 759
lemma OAI.HarmonicCounterexample.Construction.traceFree_D_trace line 766
def OAI.HarmonicCounterexample.Construction.controlScale line 772
lemma OAI.HarmonicCounterexample.Construction.controlScale_ne line 773
lemma OAI.HarmonicCounterexample.Construction.slow_toLinearMap line 776
lemma OAI.HarmonicCounterexample.Construction.D_toLinearMap line 784
lemma OAI.HarmonicCounterexample.Construction.generator_eq line 789
lemma OAI.HarmonicCounterexample.Construction.generator_trace line 798
lemma OAI.HarmonicCounterexample.Construction.generator_full line 806