OAI/Geometry/HarmonicGrowth/PulseSystem.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicCounterexample.LinearODE.finite_positive_thresholds line 11
2. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.exp_apply line 36
3. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.leftWord_apply line 41
4. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.actual_packet_apply line 52

   Source documentation

   The actual product packet has exactly the actual block packet as each factor; no norm or ODE product convention is changed in the assembly.

   lemma actual_packet_apply {n : ℕ} (a : Fin n → ℝ) (X : Fin n → MatrixProduct ι) (b : β) :
       (flow (fun t => ContinuousLinearMap.mul ℝ (MatrixProduct ι)
         (unitPacketCoefficient a X t)) 1 1) b=
       flow (fun t => ContinuousLinearMap.mul ℝ (Matrix (ι b) (ι b) ℝ)
         (unitPacketCoefficient a (fun j => X j b) t)) 1 1 := by
   …

   Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.FiniteControl.MatrixProduct, OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketCoefficient

5. theorem OAI.HarmonicCounterexample.LinearODE.compact_simultaneous_physical_C1 line 87

   Source documentation

   All retained blocks are controlled simultaneously, using one parameter ball and thresholds chosen before ANY incoming histories. Both value and outgoing slope below are the actual center-regular physical solutions.

   theorem compact_simultaneous_physical_C1 (basis : ∀ b,OrthonormalBasis (ι b) ℝ (E b))
       (hbasis : OrthonormalBasis κ ℝ H) {K : Set H} (hK : IsCompact K)
       (r p₀ γ M : ℝ) (B β θ : ξ → ℝ) (D : ∀ b,Fin n → E b →L[ℝ] E b)
       (hD : ∀ b j v,inner ℝ v (D b j v) ≤ 0)
       (hBD : ∀ b j v,-(B b*‖v‖^2) ≤ inner ℝ v (D b j v))
       (hM : 0 ≤ M) (hB : ∀ b,0 ≤ B b) (hθ : ∀ b,0 < θ b) (hγ : 0 < γ)
       (hden : ∀ b,p₀+2*θ b ≠ 0) (hroot : ∀ b,β b*B b-p₀*θ b-θ b^2=0)
       (amps : Fin n → H → ℝ) (amps' : Fin n → H → H →L[ℝ] ℝ)
       (ha : ∀ x ∈ K,∀ j,HasFDerivAt (amps j) (amps' j x) x)
       (hc : ∀ j,ContinuousOn (amps j) K) (hd : ∀ j,ContinuousOn (amps' j) K) :
       ∃ T₀ ρ C : ℝ,1 ≤ T₀ ∧ 0 < ρ ∧ 1 ≤ C ∧ ∀ T ≥ T₀,
         ∀ (history : ∀ b,ℝ → E b →L[ℝ] E b) (α drift : ℝ → ℝ)
   …

   Mentions: OAI.HarmonicCounterexample.b

6. theorem OAI.HarmonicCounterexample.LinearODE.scalar_restart_on line 161

   Source documentation

   Restart of an actual scalar second-order equation on a diagonal leg.

   theorem scalar_restart_on {A b f g : ℝ → ℝ} {c d MA Mb : ℝ}
       (hA : Continuous A) (hb : Continuous b) (hMA : 0 ≤ MA) (hMb : 0 ≤ Mb)
       (hnA : ∀ t,|A t| ≤ MA) (hnb : ∀ t,|b t| ≤ Mb)
       (hfc : ContinuousOn f (Icc c d)) (hgc : ContinuousOn g (Icc c d))
       (hf : ∀ t ∈ Ico c d,HasDerivAt f (g t) t)
       (hg : ∀ t ∈ Ico c d,HasDerivAt g (A t*f t-b t*g t) t) :
       ∀ t ∈ Icc c d,f t=
         scalarU (fun s => A (c+s)) (fun s => b (c+s)) (t-c)*f c+
         scalarV (fun s => A (c+s)) (fun s => b (c+s)) (t-c)*g c := by
   …

   Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.scalarU, OAI.HarmonicCounterexample.LinearODE.scalarV

7. def OAI.HarmonicCounterexample.LinearODE.matrixEntry line 210
8. lemma OAI.HarmonicCounterexample.LinearODE.matrixEntry_apply line 214
9. theorem OAI.HarmonicCounterexample.LinearODE.matrix_diagonal_restart line 218

   Source documentation

   Actual entrywise diagonal propagation, retaining both incoming value and velocity. No incoming stable eigenspace is imposed.

   theorem matrix_diagonal_restart {lam : ι → ℝ → ℝ} {b : ℝ → ℝ}
       {F G : ℝ → Matrix ι ι ℝ} {c d Mb : ℝ} (MA : ι → ℝ)
       (hlam : ∀ i,Continuous (lam i)) (hb : Continuous b)
       (hMA : ∀ i,0 ≤ MA i) (hMb : 0 ≤ Mb)
       (hnlam : ∀ i t,|lam i t| ≤ MA i) (hnb : ∀ t,|b t| ≤ Mb)
       (hF : ContinuousOn F (Icc c d)) (hG : ContinuousOn G (Icc c d))
       (hdF : ∀ t ∈ Ico c d,HasDerivAt F (G t) t)
       (hdG : ∀ t ∈ Ico c d,HasDerivAt G
         (Matrix.diagonal (fun i => lam i t)*F t-b t • G t) t) :
       ∀ t ∈ Icc c d,F t=
         Matrix.diagonal (fun i => scalarU (fun s => lam i (c+s)) (fun s => b (c+s)) (t-c))*F c+
         Matrix.diagonal (fun i => scalarV (fun s => lam i (c+s)) (fun s => b (c+s)) (t-c))*G c := by
   …

   Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.scalarU, OAI.HarmonicCounterexample.LinearODE.scalarV

10. theorem OAI.HarmonicCounterexample.LinearODE.actual_diagonal_restart line 256

    Source documentation

    The complete prescribed diagonal leg for the actual center-regular value fundamental matrix, not for a model first-order propagator.

    theorem actual_diagonal_restart (basis : OrthonormalBasis ι ℝ E)
        {A : ℝ → E →L[ℝ] E} {b : ℝ → ℝ} {lam : ι → ℝ → ℝ}
        {MA Mb c d : ℝ} (N : ι → ℝ) (l : ℝ)
        (hA : Continuous A) (hb : Continuous b) (hlam : ∀ i,Continuous (lam i))
        (hMA : 0 ≤ MA) (hMb : 0 ≤ Mb) (hN : ∀ i,0 ≤ N i)
        (hnA : ∀ t,‖A t‖ ≤ MA) (hnb : ∀ t,|b t| ≤ Mb) (hnlam : ∀ i t,|lam i t| ≤ N i)
        (hdiag : ∀ t ∈ Ico c d,orthogonalMatrix basis (A t)=Matrix.diagonal (fun i => lam i t)) :
        ∀ t ∈ Icc c d,orthogonalMatrix basis (operatorValue A b l t)=
          Matrix.diagonal (fun i => scalarU (fun s => lam i (c+s)) (fun s => b (c+s)) (t-c))*
            orthogonalMatrix basis (operatorValue A b l c)+
          Matrix.diagonal (fun i => scalarV (fun s => lam i (c+s)) (fun s => b (c+s)) (t-c))*
            orthogonalMatrix basis (operatorVelocity A b l c) := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix, OAI.HarmonicCounterexample.LinearODE.operatorValue, OAI.HarmonicCounterexample.LinearODE.scalarU, OAI.HarmonicCounterexample.LinearODE.scalarV, OAI.HarmonicCounterexample.LinearODE.operatorVelocity

11. def OAI.HarmonicCounterexample.LinearODE.diagonalL line 291

    Source documentation

    The fixed Frobenius-coordinate norm cost of the diagonal embedding.

    def diagonalL : (ι → ℝ) →L[ℝ] Matrix ι ι ℝ :=
    …

12. lemma OAI.HarmonicCounterexample.LinearODE.diagonalL_apply line 294
13. theorem OAI.HarmonicCounterexample.LinearODE.diagonal_leg_normalizer line 298

    Source documentation

    Exact normalization of a positive scalar diagonal leg, with a bound independent of its length and anisotropy.

    theorem diagonal_leg_normalizer (u v : ι → ℝ) {θ : ℝ}
        (hu : ∀ i,1 ≤ u i) (hv : ∀ i,0 ≤ v i) (hθ : 0 < θ) :
        ∃ D : (Matrix ι ι ℝ)ˣ,
          (D:Matrix ι ι ℝ)=Matrix.diagonal u+θ • Matrix.diagonal v ∧
          (∀ i,0 < (D:Matrix ι ι ℝ) i i) ∧
          ‖(↑D⁻¹:Matrix ι ι ℝ)*Matrix.diagonal v‖ ≤ ‖diagonalL (ι:=ι)‖*θ⁻¹ := by
    …

    Mentions: OAI.HarmonicCounterexample.LinearODE.diagonalL

14. theorem OAI.HarmonicCounterexample.LinearODE.actual_diagonal_normalizer line 353

    Source documentation

    The normalizer belongs to the ACTUAL scalar propagation columns, not freely chosen diagonal data.

    theorem actual_diagonal_normalizer {A : ι → ℝ → ℝ} {p : ℝ → ℝ}
        (hA : ∀ i,Continuous (A i)) (hp : Continuous p)
        (MA : ι → ℝ) {Mp t θ : ℝ} (hMA : ∀ i,0 ≤ MA i) (hMp : 0 ≤ Mp)
        (hAn : ∀ i s,|A i s| ≤ MA i) (hpn : ∀ s,|p s| ≤ Mp)
        (hAp : ∀ i s,0 ≤ s → 0 ≤ A i s) (ht : 0 ≤ t) (hθ : 0 < θ) :
        ∃ D : (Matrix ι ι ℝ)ˣ,
          (D:Matrix ι ι ℝ)=Matrix.diagonal (fun i => scalarU (A i) p t)+
            θ • Matrix.diagonal (fun i => scalarV (A i) p t) ∧
          (∀ i,0 < (D:Matrix ι ι ℝ) i i) ∧
          ‖(↑D⁻¹:Matrix ι ι ℝ)*Matrix.diagonal (fun i => scalarV (A i) p t)‖ ≤
            ‖diagonalL (ι:=ι)‖*θ⁻¹ := by
    …

    Mentions: OAI.HarmonicCounterexample.LinearODE.scalarU, OAI.HarmonicCounterexample.LinearODE.scalarV, OAI.HarmonicCounterexample.LinearODE.diagonalL

15. structure OAI.HarmonicCounterexample.LinearODE.PulseSystem line 387

    Source documentation

    Fixed finite angular and radial constants.

    structure PulseSystem (E : ξ → Type*) (ι : ξ → Type*) (κ : Type*)
        [∀ b,NormedAddCommGroup (E b)] [∀ b,InnerProductSpace ℝ (E b)] [∀ b,FiniteDimensional ℝ (E b)]
        [∀ b,Fintype (ι b)] [∀ b,DecidableEq (ι b)] where
    …

    Mentions: OAI.HarmonicCounterexample.b

16. def OAI.HarmonicCounterexample.LinearODE.PulseSystem.generator line 410
17. structure OAI.HarmonicCounterexample.LinearODE.PulseHistory line 415

    Source documentation

    Raw center-regular history plus the quantitative hypotheses used on the current pulse. This structure contains no transmission conclusion.

    structure PulseHistory where
    …

18. structure OAI.HarmonicCounterexample.LinearODE.PhysicalWord line 451

    Source documentation

    Fixed chronological smooth control data and a nonempty compact parameter ball. Slot count is positive; a globally zero family is not substituted.

    structure PhysicalWord (κ : Type*) where
    …

19. abbrev OAI.HarmonicCounterexample.LinearODE.PhysicalWord.Parameter line 463
20. def OAI.HarmonicCounterexample.LinearODE.PhysicalWord.ball line 464
21. def OAI.HarmonicCounterexample.LinearODE.PhysicalWord.coefficient line 466
22. def OAI.HarmonicCounterexample.LinearODE.PhysicalWord.baseline line 470
23. def OAI.HarmonicCounterexample.LinearODE.PhysicalWord.value line 473
24. def OAI.HarmonicCounterexample.LinearODE.PhysicalWord.defect line 478
25. def OAI.HarmonicCounterexample.LinearODE.PhysicalWord.ideal line 482