OAI/Geometry/HarmonicGrowth/Variation.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicCounterexample.LinearODE.actual_value_round_core line 18
2. lemma OAI.HarmonicCounterexample.LinearODE.actual_value_unit_all_time line 32

   Source documentation

   No hidden assumption of a globally invertible value evolution: positivity proves invertibility forward, and the exact Euclidean tail proves it backward.

   lemma actual_value_unit_all_time {A : ℝ → E →L[ℝ] E} {p : ℝ → ℝ}
       (hA : Continuous A) (hp : Continuous p) {MA Mp : ℝ}
       (hMA : 0 ≤ MA) (hMp : 0 ≤ Mp)
       (hAn : ∀ t,‖A t‖ ≤ MA) (hpn : ∀ t,|p t| ≤ Mp)
       (hAp : ∀ t x,0 ≤ inner ℝ x (A t x))
       {l B : ℝ} (hl : 0 < l) (hAc : ∀ t ≤ 0,∀ x,A t x=(l*(l+B)) • x)
       (hpc : ∀ t ≤ 0,p t=B) (t : ℝ) : IsUnit (operatorValue A p l t) := by
   …

   Mentions: OAI.HarmonicCounterexample.LinearODE.operatorValue

3. theorem OAI.HarmonicCounterexample.LinearODE.actual_round_reset line 48

   Source documentation

   Uniform round reset for the ACTUAL center-regular Peano--Baker solution, expressed in genuine orthonormal coordinates. Its incoming slope bound C is an arbitrary history-independent barrier, not an assumed reset conclusion.

   theorem actual_round_reset (basis : OrthonormalBasis ι ℝ E)
       {A : ℝ → E →L[ℝ] E} {p : ℝ → ℝ}
       (hA : Continuous A) (hp : Continuous p) {MA Mp : ℝ}
       (hMA : 0 ≤ MA) (hMp : 0 ≤ Mp)
       (hAn : ∀ t,‖A t‖ ≤ MA) (hpn : ∀ t,|p t| ≤ Mp)
       (hAp : ∀ t x,0 ≤ inner ℝ x (A t x))
       {l B : ℝ} (hl : 0 < l) (hAc : ∀ t ≤ 0,∀ x,A t x=(l*(l+B)) • x)
       (hpc : ∀ t ≤ 0,p t=B) {a b pmin θ M C : ℝ}
       (ha : 0 ≤ a) (hγ : 0 < pmin+θ) (hM : 0 ≤ M)
       (hpl : ∀ t ∈ Set.Icc a b,pmin ≤ p t)
       (hforce : ∀ t ∈ Set.Icc a b,
         ‖orthogonalMatrix basis (A t)-(p t*θ+θ^2) • (1 : Matrix ι ι ℝ)‖ ≤ M)
   …

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

4. def OAI.HarmonicCounterexample.LinearODE.termD line 94

   Source documentation

   Actual parameter-jet Peano–Baker terms.

   def termD (A : H → ℝ → E →L[ℝ] E) (A' : H → ℝ → H →L[ℝ] E →L[ℝ] E)
       (x : E) (p : H) : ℕ → ℝ → H →L[ℝ] E
     | 0,_ => 0
     | n+1,t => ∫ s in (0:ℝ)..t,
         (A p s).comp (termD A A' x p n s) + (A' p s).flip (term (A p) x n s)

   Mentions: OAI.HarmonicCounterexample.LinearODE.term

5. lemma OAI.HarmonicCounterexample.LinearODE.termD_continuous line 100
6. lemma OAI.HarmonicCounterexample.LinearODE.param_integrand_bound line 115
7. lemma OAI.HarmonicCounterexample.LinearODE.termD_bound line 138
8. lemma OAI.HarmonicCounterexample.LinearODE.term_hasFDerivAt_parameter line 169

   Source documentation

   Differentiate the actual iterated integrals, not an assumed parameter flow.

   lemma term_hasFDerivAt_parameter (A : H → ℝ → E →L[ℝ] E)
       (A' : H → ℝ → H →L[ℝ] E →L[ℝ] E)
       (hA : ∀ p,Continuous (A p)) (hA' : ∀ p,Continuous (A' p))
       (hdA : ∀ p t,HasFDerivAt (fun q => A q t) (A' p t) p)
       {M : ℝ} (hM : 0 ≤ M) (hb : ∀ p s,‖A p s‖ ≤ M) (hb' : ∀ p s,‖A' p s‖ ≤ M)
       (x : E) (n : ℕ) (p : H) (t : ℝ) :
       HasFDerivAt (fun q => term (A q) x n t) (termD A A' x p n t) p := by
   …

   Mentions: OAI.HarmonicCounterexample.LinearODE.term, OAI.HarmonicCounterexample.LinearODE.termD

9. theorem OAI.HarmonicCounterexample.LinearODE.flow_hasFDerivAt_parameter line 196

   Source documentation

   Genuine parameter differentiability of the global Peano–Baker solution, with an explicit convergent series for its derivative.

   theorem flow_hasFDerivAt_parameter (A : H → ℝ → E →L[ℝ] E)
       (A' : H → ℝ → H →L[ℝ] E →L[ℝ] E)
       (hA : ∀ p,Continuous (A p)) (hA' : ∀ p,Continuous (A' p))
       (hdA : ∀ p t,HasFDerivAt (fun q => A q t) (A' p t) p)
       {M : ℝ} (hM : 0 ≤ M) (hb : ∀ p s,‖A p s‖ ≤ M) (hb' : ∀ p s,‖A' p s‖ ≤ M)
       (x : E) (p : H) (t : ℝ) :
       HasFDerivAt (fun q => flow (A q) x t) (∑' n,termD A A' x p n t) p := by
   …

   Mentions: OAI.HarmonicCounterexample.LinearODE.flow, OAI.HarmonicCounterexample.LinearODE.termD

10. def OAI.HarmonicCounterexample.LinearODE.flowD line 229
11. lemma OAI.HarmonicCounterexample.LinearODE.termD_summable line 232
12. lemma OAI.HarmonicCounterexample.LinearODE.flowD_initial line 243
13. theorem OAI.HarmonicCounterexample.LinearODE.flowD_hasDerivAt line 253

    Source documentation

    The derivative in the actual control parameter satisfies the actual variational ODE, with zero initial value.

    theorem flowD_hasDerivAt (A : H → ℝ → E →L[ℝ] E)
        (A' : H → ℝ → H →L[ℝ] E →L[ℝ] E)
        (hA : ∀ p,Continuous (A p)) (hA' : ∀ p,Continuous (A' p))
        {M : ℝ} (hM : 0 ≤ M) (hb : ∀ p s,‖A p s‖ ≤ M) (hb' : ∀ p s,‖A' p s‖ ≤ M)
        (x : E) (p : H) (t : ℝ) :
        HasDerivAt (flowD A A' x p)
          ((A p t).comp (flowD A A' x p t)+(A' p t).flip (flow (A p) x t)) t := by
    …

    Mentions: OAI.HarmonicCounterexample.LinearODE.flowD, OAI.HarmonicCounterexample.LinearODE.flow

14. lemma OAI.HarmonicCounterexample.LinearODE.clm_inverse_fderiv line 327

    Source documentation

    Inversion is differentiated only at a genuinely invertible value operator.

    lemma clm_inverse_fderiv {V : H → E →L[ℝ] E} {V' : H →L[ℝ] E →L[ℝ] E} {p : H}
        (hV : IsUnit (V p)) (hD : HasFDerivAt V V' p) :
        HasFDerivAt (fun q => Ring.inverse (V q))
          ((-ContinuousLinearMap.mulLeftRight ℝ (E →L[ℝ] E)
            (Ring.inverse (V p)) (Ring.inverse (V p))).comp V') p := by
    …

15. lemma OAI.HarmonicCounterexample.LinearODE.slope_parameter_deriv line 340

    Source documentation

    The actual slope has a genuine parameter derivative, without a prior bound on that derivative. The two inputs are the actual variational value jets.

    lemma slope_parameter_deriv {V W : H → E →L[ℝ] E}
        {V' W' : H →L[ℝ] E →L[ℝ] E} {p : H}
        (hV : IsUnit (V p)) (hVD : HasFDerivAt V V' p) (hWD : HasFDerivAt W W' p) :
        HasFDerivAt (fun q => W q * Ring.inverse (V q))
          ((ContinuousLinearMap.mulLeftRight ℝ (E →L[ℝ] E) 1 (Ring.inverse (V p))).comp W' -
           (ContinuousLinearMap.mulLeftRight ℝ (E →L[ℝ] E)
             (W p * Ring.inverse (V p)) (Ring.inverse (V p))).comp V') p := by
    …

16. theorem OAI.HarmonicCounterexample.LinearODE.actual_slope_hasFDerivAt line 368

    Source documentation

    Apply the global actual-flow parameter differentiability theorem to the center-regular second-order operator system. The coefficient derivative is explicit data and must be an actual Frechet derivative, never an assumed slope.

    theorem actual_slope_hasFDerivAt
        (A : H → ℝ → E →L[ℝ] E) (b : ℝ → ℝ)
        (B' : H → ℝ → H →L[ℝ] (((E →L[ℝ] E)×(E →L[ℝ] E)) →L[ℝ]
          ((E →L[ℝ] E)×(E →L[ℝ] E))))
        (hA : ∀ p,Continuous (A p)) (hb : Continuous b)
        (hB' : ∀ p,Continuous (B' p))
        (hdB : ∀ p t,HasFDerivAt (fun q => block (leftAction (A q)) b t) (B' p t) p)
        {M : ℝ} (hM : 0 ≤ M)
        (hnB : ∀ p t,‖block (leftAction (A p)) b t‖ ≤ M)
        (hnB' : ∀ p t,‖(B' p t : H →L[ℝ] (((E →L[ℝ] E)×(E →L[ℝ] E)) →L[ℝ]
          ((E →L[ℝ] E)×(E →L[ℝ] E))))‖ ≤ M)
        (l : ℝ) (p : H) (t : ℝ) (hV : IsUnit (operatorValue (A p) b l t)) :
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.block, OAI.HarmonicCounterexample.LinearODE.leftAction, OAI.HarmonicCounterexample.LinearODE.operatorValue

17. lemma OAI.HarmonicCounterexample.LinearODE.ring_inverse_deriv line 405
18. theorem OAI.HarmonicCounterexample.LinearODE.variation_slope_deriv line 418

    Source documentation

    Genuine time evolution of the logarithmic derivative of a variational value solution. This is applied to the already constructed actual first jet.

    theorem variation_slope_deriv (A P Y U V A₁ p : ℝ → R) {t : ℝ}
        (hY : HasDerivAt Y (P t*Y t) t)
        (hP : HasDerivAt P (A t-p t*P t-P t*P t) t)
        (hU : HasDerivAt U (V t) t)
        (hV : HasDerivAt V (A₁ t*Y t+A t*U t-p t*V t) t)
        (hy : IsUnit (Y t)) :
        HasDerivAt (fun s => (V s-P s*U s)*Ring.inverse (Y s))
          (A₁ t-p t*((V t-P t*U t)*Ring.inverse (Y t))-
            P t*((V t-P t*U t)*Ring.inverse (Y t))-
            ((V t-P t*U t)*Ring.inverse (Y t))*P t) t := by
    …

19. theorem OAI.HarmonicCounterexample.LinearODE.riccati_parameter_regroup line 443

    Source documentation

    The crucial regrouping of the parameter-error equation. Both sides damp with the actual positive regular slope P; no bound on its derivative is used.

    theorem riccati_parameter_regroup (A₁ p P Q P₁ Q₁ Q₁' : R) :
        (A₁-p*P₁-P*P₁-P₁*P)-Q₁' =
          (A₁-p*Q₁-Q₁*Q-Q*Q₁-Q₁')-
            (p+P)*(P₁-Q₁)-(P₁-Q₁)*P-Q₁*(P-Q)-(P-Q)*Q₁ := by
    …

20. abbrev OAI.HarmonicCounterexample.LinearODE.OperatorPhase line 471
21. def OAI.HarmonicCounterexample.LinearODE.phaseJet line 474
22. def OAI.HarmonicCounterexample.LinearODE.valueJet line 479
23. def OAI.HarmonicCounterexample.LinearODE.velocityJet line 484
24. def OAI.HarmonicCounterexample.LinearODE.slopeJet line 489
25. lemma OAI.HarmonicCounterexample.LinearODE.slopeJet_apply line 498
26. theorem OAI.HarmonicCounterexample.LinearODE.slope_hasFDerivAt_jet line 508

    Source documentation

    Explicit actual parameter derivative of the actual global regular slope.

    theorem slope_hasFDerivAt_jet
        (A : H → ℝ → E →L[ℝ] E) (b : ℝ → ℝ)
        (B' : H → ℝ → H →L[ℝ] OperatorPhase E →L[ℝ] OperatorPhase E)
        (hA : ∀ p,Continuous (A p)) (hb : Continuous b) (hB' : ∀ p,Continuous (B' p))
        (hdB : ∀ p t,HasFDerivAt (fun q => block (leftAction (A q)) b t) (B' p t) p)
        {M : ℝ} (hM : 0 ≤ M) (hnB : ∀ p t,‖block (leftAction (A p)) b t‖ ≤ M)
        (hnB' : ∀ p t,‖B' p t‖ ≤ M)
        (l : ℝ) (p : H) (t : ℝ) (hV : IsUnit (operatorValue (A p) b l t)) :
        HasFDerivAt (fun q => slope (A q) b l t) (slopeJet A b B' l p t) p := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.OperatorPhase, OAI.HarmonicCounterexample.LinearODE.block, OAI.HarmonicCounterexample.LinearODE.leftAction, OAI.HarmonicCounterexample.LinearODE.operatorValue, OAI.HarmonicCounterexample.LinearODE.slope, OAI.HarmonicCounterexample.LinearODE.slopeJet

27. theorem OAI.HarmonicCounterexample.LinearODE.slopeJet_hasDerivAt line 527

    Source documentation

    The actual center-regular parameter jet evolves by the damped Riccati variational equation. There is no assumed bound on this jet.

    theorem slopeJet_hasDerivAt
        (A : H → ℝ → E →L[ℝ] E) (b : ℝ → ℝ)
        (B' : H → ℝ → H →L[ℝ] OperatorPhase E →L[ℝ] OperatorPhase E)
        (A' : H → ℝ → H →L[ℝ] E →L[ℝ] E)
        (hA : ∀ p,Continuous (A p)) (hb : Continuous b) (hB' : ∀ p,Continuous (B' p))
        (hBeval : ∀ p t h v,B' p t h v=(0,A' p t h*v.1))
        {M MA Mb : ℝ} (hM : 0 ≤ M) (hMA : 0 ≤ MA) (hMb : 0 ≤ Mb)
        (hnB : ∀ p t,‖block (leftAction (A p)) b t‖ ≤ M) (hnB' : ∀ p t,‖B' p t‖ ≤ M)
        (hnA : ∀ p t,‖A p t‖ ≤ MA) (hnb : ∀ t,|b t| ≤ Mb)
        (l : ℝ) (p h : H) (t : ℝ) (hV : IsUnit (operatorValue (A p) b l t)) :
        HasDerivAt (fun s => slopeJet A b B' l p s h)
          (A' p t h-b t • slopeJet A b B' l p t h-
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.OperatorPhase, OAI.HarmonicCounterexample.LinearODE.block, OAI.HarmonicCounterexample.LinearODE.leftAction, OAI.HarmonicCounterexample.LinearODE.operatorValue, OAI.HarmonicCounterexample.LinearODE.slopeJet

28. lemma OAI.HarmonicCounterexample.LinearODE.slopeJet_initial line 570
29. lemma OAI.HarmonicCounterexample.LinearODE.termD_frozen line 594
30. lemma OAI.HarmonicCounterexample.LinearODE.flowD_frozen line 602
31. lemma OAI.HarmonicCounterexample.LinearODE.slopeJet_frozen line 630
32. theorem OAI.HarmonicCounterexample.LinearODE.slopeJet_hasDerivAt_pointwise line 641

    Source documentation

    Actual directional slope jets need bounds only at the current parameter. This avoids imposing nonexistent global bounds on the full control parameter space outside the admissible ball.

    theorem slopeJet_hasDerivAt_pointwise
        (A : H → ℝ → E →L[ℝ] E) (b : ℝ → ℝ)
        (B' : H → ℝ → H →L[ℝ] OperatorPhase E →L[ℝ] OperatorPhase E)
        (A' : H → ℝ → H →L[ℝ] E →L[ℝ] E) (p h : H)
        (hA : Continuous (A p)) (hb : Continuous b) (hB' : Continuous (B' p))
        (hBeval : ∀ t z v,B' p t z v=(0,A' p t z*v.1))
        {M MA Mb : ℝ} (hM : 0 ≤ M) (hMA : 0 ≤ MA) (hMb : 0 ≤ Mb)
        (hnB : ∀ t,‖block (leftAction (A p)) b t‖ ≤ M) (hnB' : ∀ t,‖B' p t‖ ≤ M)
        (hnA : ∀ t,‖A p t‖ ≤ MA) (hnb : ∀ t,|b t| ≤ Mb)
        (l : ℝ) (t : ℝ) (hV : IsUnit (operatorValue (A p) b l t)) :
        HasDerivAt (fun s => slopeJet A b B' l p s h)
          (A' p t h-b t • slopeJet A b B' l p t h-
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.OperatorPhase, OAI.HarmonicCounterexample.LinearODE.block, OAI.HarmonicCounterexample.LinearODE.leftAction, OAI.HarmonicCounterexample.LinearODE.operatorValue, OAI.HarmonicCounterexample.LinearODE.slopeJet

33. theorem OAI.HarmonicCounterexample.LinearODE.actual_slow_pulse_integrated line 689

    Source documentation

    Uniform-history L1 value and first-jet error for the ACTUAL center-regular Peano--Baker solution. Coercivity of the unknown Riccati solution is PRODUCED from positivity and its Euclidean core; neither a solution nor an unknown-jet bound is supplied as a hypothesis. The comparison residuals are explicit.

    theorem actual_slow_pulse_integrated (basis : OrthonormalBasis ι ℝ E)
        (A : H → ℝ → E →L[ℝ] E) (b : ℝ → ℝ)
        (B' : H → ℝ → H →L[ℝ] OperatorPhase E →L[ℝ] OperatorPhase E)
        (A' : H → ℝ → H →L[ℝ] E →L[ℝ] E) (p h : H)
        (hA : Continuous (A p)) (hb : Continuous b) (hB' : Continuous (B' p))
        (hA' : Continuous (fun t => A' p t h))
        (hBeval : ∀ t z v,B' p t z v=(0,A' p t z*v.1))
        {M MA Mb : ℝ} (hM : 0 ≤ M) (hMA : 0 ≤ MA) (hMb : 0 ≤ Mb)
        (hnB : ∀ t,‖block (leftAction (A p)) b t‖ ≤ M) (hnB' : ∀ t,‖B' p t‖ ≤ M)
        (hnA : ∀ t,‖A p t‖ ≤ MA) (hnb : ∀ t,|b t| ≤ Mb)
        (hAp : ∀ t x,0 ≤ inner ℝ x (A p t x))
        {l B : ℝ} (hl : 0 < l) (hAc : ∀ t ≤ 0,∀ x,A p t x=(l*(l+B)) • x)
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.OperatorPhase, OAI.HarmonicCounterexample.LinearODE.block, OAI.HarmonicCounterexample.LinearODE.leftAction

34. lemma OAI.HarmonicCounterexample.LinearODE.termD_continuous_at_parameter line 778
35. lemma OAI.HarmonicCounterexample.LinearODE.param_integrand_bound_at_parameter line 793
36. lemma OAI.HarmonicCounterexample.LinearODE.termD_bound_at_parameter line 816
37. lemma OAI.HarmonicCounterexample.LinearODE.term_hasFDerivAt_parameter_on line 849

    Source documentation

    Local-parameter differentiation of actual Peano--Baker iterates. The coefficient bounds are only required on the genuine admissible parameter set.

    lemma term_hasFDerivAt_parameter_on (A : H → ℝ → E →L[ℝ] E)
        (A' : H → ℝ → H →L[ℝ] E →L[ℝ] E) {S : Set H} (hS : IsOpen S)
        (hA : ∀ p ∈ S,Continuous (A p)) (hA' : ∀ p ∈ S,Continuous (A' p))
        (hdA : ∀ p ∈ S,∀ t,HasFDerivAt (fun q => A q t) (A' p t) p)
        {M : ℝ} (hM : 0 ≤ M) (hb : ∀ p ∈ S,∀ s,‖A p s‖ ≤ M)
        (hb' : ∀ p ∈ S,∀ s,‖A' p s‖ ≤ M)
        (x : E) (n : ℕ) {p : H} (hp : p ∈ S) (t : ℝ) :
        HasFDerivAt (fun q => term (A q) x n t) (termD A A' x p n t) p := by
    …

    Mentions: OAI.HarmonicCounterexample.LinearODE.term, OAI.HarmonicCounterexample.LinearODE.termD

38. theorem OAI.HarmonicCounterexample.LinearODE.flow_hasFDerivAt_parameter_on line 879

    Source documentation

    The actual flow is C1-differentiable on an admissible open connected ball; no uniformity over inadmissible or arbitrarily large control parameters occurs.

    theorem flow_hasFDerivAt_parameter_on (A : H → ℝ → E →L[ℝ] E)
        (A' : H → ℝ → H →L[ℝ] E →L[ℝ] E) {S : Set H}
        (hS : IsOpen S) (hSc : IsPreconnected S)
        (hA : ∀ p ∈ S,Continuous (A p)) (hA' : ∀ p ∈ S,Continuous (A' p))
        (hdA : ∀ p ∈ S,∀ t,HasFDerivAt (fun q => A q t) (A' p t) p)
        {M : ℝ} (hM : 0 ≤ M) (hb : ∀ p ∈ S,∀ s,‖A p s‖ ≤ M)
        (hb' : ∀ p ∈ S,∀ s,‖A' p s‖ ≤ M)
        (x : E) {p : H} (hp : p ∈ S) (t : ℝ) :
        HasFDerivAt (fun q => flow (A q) x t) (flowD A A' x p t) p := by
    …

    Mentions: OAI.HarmonicCounterexample.LinearODE.flow, OAI.HarmonicCounterexample.LinearODE.flowD

39. theorem OAI.HarmonicCounterexample.LinearODE.slope_hasFDerivAt_jet_on line 924

    Source documentation

    The variational slope in the quantitative estimates is the GENUINE Frechet derivative of the actual PB slope on the admissible parameter ball. The hypotheses only require bounds on that ball, never outside it.

    theorem slope_hasFDerivAt_jet_on
        (A : H → ℝ → E →L[ℝ] E) (b : ℝ → ℝ)
        (B' : H → ℝ → H →L[ℝ] OperatorPhase E →L[ℝ] OperatorPhase E)
        {S : Set H} (hS : IsOpen S) (hSc : IsPreconnected S)
        (hA : ∀ p ∈ S,Continuous (A p)) (hb : Continuous b) (hB' : ∀ p ∈ S,Continuous (B' p))
        (hdB : ∀ p ∈ S,∀ t,HasFDerivAt (fun q => block (leftAction (A q)) b t) (B' p t) p)
        {M : ℝ} (hM : 0 ≤ M) (hnB : ∀ p ∈ S,∀ t,‖block (leftAction (A p)) b t‖ ≤ M)
        (hnB' : ∀ p ∈ S,∀ t,‖B' p t‖ ≤ M)
        (l : ℝ) {p : H} (hp : p ∈ S) (t : ℝ) (hV : IsUnit (operatorValue (A p) b l t)) :
        HasFDerivAt (fun q => slope (A q) b l t) (slopeJet A b B' l p t) p := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.OperatorPhase, OAI.HarmonicCounterexample.LinearODE.block, OAI.HarmonicCounterexample.LinearODE.leftAction, OAI.HarmonicCounterexample.LinearODE.operatorValue, OAI.HarmonicCounterexample.LinearODE.slope, OAI.HarmonicCounterexample.LinearODE.slopeJet

40. theorem OAI.HarmonicCounterexample.LinearODE.dissipative_integral_on line 961

    Source documentation

    Local-in-time integrated damping. A constant exterior extension is applied only to the scalar integrand, not to the differentiable unknown. Consequently no artificial globally nonsingular comparison Riccati solution is required.

    theorem dissipative_integral_on {f f' : ℝ → E} {r : ℝ → ℝ} {c a b : ℝ}
        (hab : a ≤ b) (hf : ∀ t ∈ Icc a b,HasDerivAt f (f' t) t)
        (hr : ContinuousOn r (Icc a b))
        (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

41. theorem OAI.HarmonicCounterexample.LinearODE.dissipative_gronwall_on line 1000

    Source documentation

    The sharp exponential bound only uses derivatives ON the pulse interval.

    theorem dissipative_gronwall_on {f f' : ℝ → E} {c M a b : ℝ}
        (hf : ∀ t ∈ Icc a b,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

42. theorem OAI.HarmonicCounterexample.LinearODE.sylvester_integrated_on line 1029

    Source documentation

    Sharp integrated Sylvester damping in the actual Frobenius matrix norm.

    theorem sylvester_integrated_on {X F L R : ℝ → Matrix ι ι ℝ} {a b c d : ℝ}
        (hab : a ≤ b) (hF : ContinuousOn F (Set.Icc a b))
        (hX : ∀ t ∈ Set.Icc a b,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

43. theorem OAI.HarmonicCounterexample.LinearODE.sylvester_gronwall_on line 1057

    Source documentation

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

    theorem sylvester_gronwall_on {X F L R : ℝ → Matrix ι ι ℝ} {a b c d M : ℝ}
        (hX : ∀ t ∈ Set.Icc a b,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

44. theorem OAI.HarmonicCounterexample.LinearODE.sylvester_jet_integrated_on line 1087

    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_on {Z X ρ Q L R : ℝ → Matrix ι ι ℝ} {a b c d q : ℝ}
        (hab : a ≤ b) (hρ : ContinuousOn ρ (Set.Icc a b)) (hQ : ContinuousOn Q (Set.Icc a b)) (hX : ContinuousOn X (Set.Icc a b))
        (hZ : ∀ t ∈ Set.Icc a b,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

45. theorem OAI.HarmonicCounterexample.LinearODE.slow_pulse_error_estimate_on line 1119

    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_on
        {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ρ : ContinuousOn ρ (Icc a (a+T))) (hρ₁ : ContinuousOn ρ₁ (Icc a (a+T))) (hQ₁ : ContinuousOn Q₁ (Icc a (a+T)))
        (hX : ∀ t ∈ Icc a (a+T),HasDerivAt X (ρ t-(L t*X t+X t*R t)) t)
        (hZ : ∀ t ∈ Icc a (a+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

46. theorem OAI.HarmonicCounterexample.LinearODE.actual_slow_pulse_integrated_on line 1236

    Source documentation

    Uniform-history L1 value and first-jet error for the ACTUAL center-regular Peano--Baker solution. Coercivity of the unknown Riccati solution is PRODUCED from positivity and its Euclidean core; neither a solution nor an unknown-jet bound is supplied as a hypothesis. The comparison residuals are explicit.

    theorem actual_slow_pulse_integrated_on (basis : OrthonormalBasis ι ℝ E)
        (A : H → ℝ → E →L[ℝ] E) (b : ℝ → ℝ)
        (B' : H → ℝ → H →L[ℝ] OperatorPhase E →L[ℝ] OperatorPhase E)
        (A' : H → ℝ → H →L[ℝ] E →L[ℝ] E) (p h : H)
        (hA : Continuous (A p)) (hb : Continuous b) (hB' : Continuous (B' p))
        (hA' : Continuous (fun t => A' p t h))
        (hBeval : ∀ t z v,B' p t z v=(0,A' p t z*v.1))
        {M MA Mb : ℝ} (hM : 0 ≤ M) (hMA : 0 ≤ MA) (hMb : 0 ≤ Mb)
        (hnB : ∀ t,‖block (leftAction (A p)) b t‖ ≤ M) (hnB' : ∀ t,‖B' p t‖ ≤ M)
        (hnA : ∀ t,‖A p t‖ ≤ MA) (hnb : ∀ t,|b t| ≤ Mb)
        (hAp : ∀ t x,0 ≤ inner ℝ x (A p t x))
        {l B : ℝ} (hl : 0 < l) (hAc : ∀ t ≤ 0,∀ x,A p t x=(l*(l+B)) • x)
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.OperatorPhase, OAI.HarmonicCounterexample.LinearODE.block, OAI.HarmonicCounterexample.LinearODE.leftAction

47. theorem OAI.HarmonicCounterexample.LinearODE.actual_slow_pulse_estimates_on line 1313