OAI/Geometry/HarmonicGrowth/Damping.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicCounterexample.LinearODE.orthogonalMatrixLinear line 19

   Source documentation

   An actual orthonormal coordinate map for continuous real endomorphisms.

   def orthogonalMatrixLinear (b : OrthonormalBasis ι ℝ E) :
       (E →L[ℝ] E) →ₗ[ℝ] Matrix ι ι ℝ where
   …

   Mentions: OAI.HarmonicCounterexample.b

2. def OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix line 25
3. lemma OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix_apply line 29
4. lemma OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix_mul line 35
5. lemma OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix_one line 41
6. lemma OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix_mulVec line 46
7. lemma OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix_coercive line 55

   Source documentation

   Quadratic positivity is transported exactly; no equivalence-of-norms constant contaminates the damping rate.

   lemma orthogonalMatrix_coercive (b : OrthonormalBasis ι ℝ E) (T : E →L[ℝ] E)
       {c : ℝ} (hT : ∀ x,c*‖x‖^2 ≤ inner ℝ x (T x)) (v : ι → ℝ) :
       c*(∑ i,(v i)^2) ≤ ∑ i,∑ j,v i*orthogonalMatrix b T i j*v j := by
   …

   Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix

8. lemma OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix_hasDerivAt line 81

   Source documentation

   Differentiation of coordinate matrices is the genuine continuous-linear chain rule, for both time and parameter derivatives.

   lemma orthogonalMatrix_hasDerivAt (b : OrthonormalBasis ι ℝ E)
       {f : ℝ → E →L[ℝ] E} {f' : E →L[ℝ] E} {t : ℝ} (hf : HasDerivAt f f' t) :
       HasDerivAt (fun s => orthogonalMatrix b (f s)) (orthogonalMatrix b f') t :=
   …

   Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix

9. lemma OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix_riccati_deriv line 86
10. lemma OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix_jet_deriv line 94
11. lemma OAI.HarmonicCounterexample.LinearODE.norm_deriv_of_ne_zero line 118
12. lemma OAI.HarmonicCounterexample.LinearODE.dissipative_norm_slope line 125

    Source documentation

    The norm has the sharp right upper slope, including at its zeros.

    lemma dissipative_norm_slope {f f' : ℝ → E} {r : ℝ → ℝ} {c t : ℝ}
        (hf : HasDerivAt f (f' t) t)
        (he : ⟪f t,f' t⟫_ℝ ≤ -c*‖f t‖^2+r t*‖f t‖)
        (hz : f t = 0 → ‖f' t‖ ≤ r t) :
        ∀ z, -c*‖f t‖+r t < z → ∃ᶠ s in 𝓝[>] t,
          (s-t)⁻¹*(‖f s‖-‖f t‖) < z := by
    …

13. theorem OAI.HarmonicCounterexample.LinearODE.dissipative_integral line 145

    Source documentation

    Exact integrated forced damping, with neither a missing zero case nor an assumed scalar differential inequality for the nondifferentiable norm.

    theorem dissipative_integral {f f' : ℝ → E} {r : ℝ → ℝ} {c a b : ℝ}
        (hab : a ≤ b) (hf : ∀ t, HasDerivAt f (f' t) t) (hr : Continuous r)
        (he : ∀ t ∈ Icc a b, ⟪f t,f' t⟫_ℝ ≤ -c*‖f t‖^2+r t*‖f t‖)
        (hz : ∀ t ∈ Icc a b,f t = 0 → ‖f' t‖ ≤ r t) :
        c*(∫ t in a..b, ‖f t‖) ≤ ‖f a‖-‖f b‖+∫ t in a..b,r t := by
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.b

14. theorem OAI.HarmonicCounterexample.LinearODE.dissipative_gronwall line 174

    Source documentation

    Uniformly forced exponential reset in a Hilbert space. The damping constant may have either sign in the general comparison theorem.

    theorem dissipative_gronwall {f f' : ℝ → E} {c M a b : ℝ}
        (hf : ∀ t, HasDerivAt f (f' t) t)
        (he : ∀ t ∈ Icc a b, ⟪f t,f' t⟫_ℝ ≤ -c*‖f t‖^2+M*‖f t‖)
        (hz : ∀ t ∈ Icc a b,f t = 0 → ‖f' t‖ ≤ M) :
        ∀ t ∈ Icc a b, ‖f t‖ ≤ gronwallBound ‖f a‖ (-c) M (t-a) := by
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.b

15. lemma OAI.HarmonicCounterexample.LinearODE.dissipative_rhs line 187

    Source documentation

    A coercive linear damping operator supplies every hypothesis above.

    lemma dissipative_rhs {F x : E} {L : E →L[ℝ] E} {c : ℝ}
        (hL : c*‖x‖^2 ≤ ⟪x,L x⟫_ℝ) :
        ⟪x,F-L x⟫_ℝ ≤ -c*‖x‖^2+‖F‖*‖x‖ := by
    …

16. def OAI.HarmonicCounterexample.LinearODE.frobenius line 212

    Source documentation

    Actual Hilbert--Schmidt coordinates, not the operator norm silently endowed with a Hilbert inner product.

    def frobenius (M : Matrix ι ι ℝ) : EuclideanSpace ℝ (ι×ι) :=
    …

17. lemma OAI.HarmonicCounterexample.LinearODE.frobenius_inner line 215
18. lemma OAI.HarmonicCounterexample.LinearODE.frobenius_norm_sq line 225
19. lemma OAI.HarmonicCounterexample.LinearODE.sylvester_coercive line 232

    Source documentation

    Coercivity of both sides of the actual Sylvester damping operator. This is the uniform positive constant used in the Riccati error equation.

    lemma sylvester_coercive {A B : Matrix ι ι ℝ} {a b : ℝ}
        (hA : ∀ v : ι → ℝ, a*(∑ i,(v i)^2) ≤ ∑ i,∑ j,v i*A i j*v j)
        (hB : ∀ v : ι → ℝ, b*(∑ i,(v i)^2) ≤ ∑ i,∑ j,v i*B i j*v j)
        (X : Matrix ι ι ℝ) :
        (a+b)*‖frobenius X‖^2 ≤ ⟪frobenius X,frobenius (A*X+X*B)⟫_ℝ := by
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.frobenius

20. def OAI.HarmonicCounterexample.LinearODE.frobeniusLinear line 288
21. def OAI.HarmonicCounterexample.LinearODE.frobeniusCLM line 293
22. lemma OAI.HarmonicCounterexample.LinearODE.frobeniusCLM_apply line 297
23. lemma OAI.HarmonicCounterexample.LinearODE.frobenius_norm line 299
24. lemma OAI.HarmonicCounterexample.LinearODE.frobenius_injective line 304
25. theorem OAI.HarmonicCounterexample.LinearODE.sylvester_integrated line 310

    Source documentation

    Sharp integrated Sylvester damping in the actual Frobenius matrix norm.

    theorem sylvester_integrated {X F L R : ℝ → Matrix ι ι ℝ} {a b c d : ℝ}
        (hab : a ≤ b) (hF : Continuous F)
        (hX : ∀ t,HasDerivAt X (F t-(L t*X t+X t*R t)) t)
        (hL : ∀ t ∈ Set.Icc a b,∀ v : ι → ℝ,
          c*(∑ i,(v i)^2) ≤ ∑ i,∑ j,v i*L t i j*v j)
        (hR : ∀ t ∈ Set.Icc a b,∀ v : ι → ℝ,
          d*(∑ i,(v i)^2) ≤ ∑ i,∑ j,v i*R t i j*v j) :
        (c+d)*(∫ t in a..b,‖X t‖) ≤ ‖X a‖-‖X b‖+∫ t in a..b,‖F t‖ := by
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.b

26. theorem OAI.HarmonicCounterexample.LinearODE.sylvester_gronwall line 338

    Source documentation

    Uniform forced damping, with the exact exponentially decaying initial term.

    theorem sylvester_gronwall {X F L R : ℝ → Matrix ι ι ℝ} {a b c d M : ℝ}
        (hX : ∀ t,HasDerivAt X (F t-(L t*X t+X t*R t)) t)
        (hF : ∀ t ∈ Set.Icc a b,‖F t‖ ≤ M)
        (hL : ∀ t ∈ Set.Icc a b,∀ v : ι → ℝ,
          c*(∑ i,(v i)^2) ≤ ∑ i,∑ j,v i*L t i j*v j)
        (hR : ∀ t ∈ Set.Icc a b,∀ v : ι → ℝ,
          d*(∑ i,(v i)^2) ≤ ∑ i,∑ j,v i*R t i j*v j) :
        ∀ t ∈ Set.Icc a b,‖X t‖ ≤ gronwallBound ‖X a‖ (-(c+d)) M (t-a) := by
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.b

27. lemma OAI.HarmonicCounterexample.LinearODE.jet_forcing_norm line 385

    Source documentation

    The parameter forcing has one small coefficient multiplying the VALUE error. This estimate never introduces the unknown size of the slope derivative.

    lemma jet_forcing_norm (ρ Q X : Matrix ι ι ℝ) {q : ℝ} (hQ : ‖Q‖ ≤ q) :
        ‖ρ-Q*X-X*Q‖ ≤ ‖ρ‖+2*q*‖X‖ := by
    …

28. theorem OAI.HarmonicCounterexample.LinearODE.sylvester_jet_integrated line 398

    Source documentation

    Integrated first-parameter error, driven by integrated VALUE error rather than pulse duration times its initial size. This is the source's C1 mechanism.

    theorem sylvester_jet_integrated {Z X ρ Q L R : ℝ → Matrix ι ι ℝ} {a b c d q : ℝ}
        (hab : a ≤ b) (hρ : Continuous ρ) (hQ : Continuous Q) (hX : Continuous X)
        (hZ : ∀ t,HasDerivAt Z ((ρ t-Q t*X t-X t*Q t)-(L t*Z t+Z t*R t)) t)
        (hQn : ∀ t ∈ Set.Icc a b,‖Q t‖ ≤ q)
        (hL : ∀ t ∈ Set.Icc a b,∀ v : ι → ℝ,
          c*(∑ i,(v i)^2) ≤ ∑ i,∑ j,v i*L t i j*v j)
        (hR : ∀ t ∈ Set.Icc a b,∀ v : ι → ℝ,
          d*(∑ i,(v i)^2) ≤ ∑ i,∑ j,v i*R t i j*v j) :
        (c+d)*(∫ t in a..b,‖Z t‖) ≤
          ‖Z a‖+(∫ t in a..b,‖ρ t‖)+2*q*(∫ t in a..b,‖X t‖) := by
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.b

29. theorem OAI.HarmonicCounterexample.LinearODE.integrated_error_pair line 428

    Source documentation

    An explicit, dimension-independent-in-time C1 integrated error constant. All norms are honest Frobenius norms; no time interval is hidden in the constant.

    theorem integrated_error_pair {IX IZ Iρ Iρ₁ X₀ Z₀ γ q : ℝ}
        (hγ : 0 < γ) (hq : 0 ≤ q)
        (hX : γ*IX ≤ X₀+Iρ) (hZ : γ*IZ ≤ Z₀+Iρ₁+2*q*IX) :
        IX ≤ (X₀+Iρ)/γ ∧
          IZ ≤ (Z₀+Iρ₁)/γ+2*q*(X₀+Iρ)/γ^2 := by
    …

30. lemma OAI.HarmonicCounterexample.LinearODE.riccati_error_deriv line 462

    Source documentation

    The difference of the ACTUAL Riccati solution and any differentiable comparison function satisfies the two-sided damped equation.

    lemma riccati_error_deriv {P Q : ℝ → R} {A Q' : R} {p t : ℝ}
        (hP : HasDerivAt P (A-p • P t-P t*P t) t)
        (hQ : HasDerivAt Q Q' t) :
        HasDerivAt (fun s => P s-Q s)
          ((A-p • Q t-Q t*Q t-Q')-
            (((p • (1:R))+P t)*(P t-Q t)+(P t-Q t)*Q t)) t := by
    …

31. lemma OAI.HarmonicCounterexample.LinearODE.riccati_error_jet_deriv line 474

    Source documentation

    The first parameter difference damps with P on BOTH sides. This is why one does not need a prior bound on the actual slope derivative.

    lemma riccati_error_jet_deriv {P₁ Q₁ : ℝ → R} {A₁ P Q Q₁' : R} {p t : ℝ}
        (hP : HasDerivAt P₁ (A₁-p • P₁ t-P*P₁ t-P₁ t*P) t)
        (hQ : HasDerivAt Q₁ Q₁' t) :
        HasDerivAt (fun s => P₁ s-Q₁ s)
          (((A₁-p • Q₁ t-Q₁ t*Q-Q*Q₁ t-Q₁')-Q₁ t*(P-Q)-(P-Q)*Q₁ t)-
            ((p • (1:R)+P)*(P₁ t-Q₁ t)+(P₁ t-Q₁ t)*P)) t := by
    …

32. lemma OAI.HarmonicCounterexample.LinearODE.damped_gronwall_bound line 501
33. theorem OAI.HarmonicCounterexample.LinearODE.slow_pulse_error_estimate line 522

    Source documentation

    Quantitative source slow-pulse estimate, retaining both integrated errors and the smaller pointwise parameter error. Its hypotheses are the two proved error equations and coefficient residual bounds, NOT a bound on the unknown jet. C is a single uniform constant and T is the genuine pulse duration.

    theorem slow_pulse_error_estimate
        {X Z ρ ρ₁ Q₁ L R L₁ R₁ : ℝ → Matrix ι ι ℝ}
        {a T γ c d c₁ d₁ C η : ℝ}
        (hT : 1 ≤ T) (hγ : 0 < γ) (hC : 0 ≤ C) (hη : 0 ≤ η)
        (hcd : c+d=γ) (hcd₁ : c₁+d₁=γ)
        (hρ : Continuous ρ) (hρ₁ : Continuous ρ₁) (hQ₁ : Continuous Q₁)
        (hX : ∀ t,HasDerivAt X (ρ t-(L t*X t+X t*R t)) t)
        (hZ : ∀ t,HasDerivAt Z ((ρ₁ t-Q₁ t*X t-X t*Q₁ t)-(L₁ t*Z t+Z t*R₁ t)) t)
        (hbρ : ∀ t ∈ Icc a (a+T),‖ρ t‖ ≤ C*η/T)
        (hbρ₁ : ∀ t ∈ Icc a (a+T),‖ρ₁ t‖ ≤ C*η/T)
        (hbQ₁ : ∀ t ∈ Icc a (a+T),‖Q₁ t‖ ≤ C/T)
        (hL : ∀ t ∈ Icc a (a+T),∀ v : ι → ℝ,
    …

    Mentions: OAI.HarmonicCounterexample.a

34. lemma OAI.HarmonicCounterexample.LinearODE.quadratic_scalar_one line 626
35. lemma OAI.HarmonicCounterexample.LinearODE.quadratic_add line 636
36. theorem OAI.HarmonicCounterexample.LinearODE.round_reset_estimate line 644

    Source documentation

    Genuine uniform reset including its exponentially decaying history term. Only coefficient-size and Riccati positivity bounds are required; there is no assumed closeness of the incoming slope to the round root.

    theorem round_reset_estimate {A P : ℝ → Matrix ι ι ℝ} {p : ℝ → ℝ}
        {a b pmin α θ M C : ℝ}
        (hγ : 0 < pmin+α+θ) (hM : 0 ≤ M)
        (hP : ∀ t,HasDerivAt P (A t-p t • P t-P t*P t) t)
        (hp : ∀ t ∈ Icc a b,pmin ≤ p t)
        (hpos : ∀ t ∈ Icc a b,∀ v : ι → ℝ,
          α*(∑ i,(v i)^2) ≤ ∑ i,∑ j,v i*P t i j*v j)
        (hforce : ∀ t ∈ Icc a b,
          ‖A t-(p t*θ+θ^2) • (1 : Matrix ι ι ℝ)‖ ≤ M)
        (hinit : ‖P a-θ • (1 : Matrix ι ι ℝ)‖ ≤ C) :
        ∀ t ∈ Icc a b,
          ‖P t-θ • (1 : Matrix ι ι ℝ)‖ ≤
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.b