OAI/Geometry/HarmonicGrowth/Transmission.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix_injective line 21
2. theorem OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix_norm_bound line 35

   Source documentation

   A fixed coordinate norm constant, chosen independently of the pulse, its duration, its history and its parameters.

   theorem orthogonalMatrix_norm_bound (b : OrthonormalBasis ι ℝ E) :
       ∃ C : ℝ,0 < C ∧ ∀ T : E →L[ℝ] E,‖T‖ ≤ C*‖orthogonalMatrix b T‖ := by
   …

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

3. lemma OAI.HarmonicCounterexample.LinearODE.integrated_matrix_error_to_operator line 41
4. lemma OAI.HarmonicCounterexample.LinearODE.bounded_target_log line 76

   Source documentation

   The bounded exact positive scalar from local attainment has a UNIFORM logarithm cost. It cannot become exponentially small along histories.

   lemma bounded_target_log {c : ℝ} (hc : c ∈ Ioo (1/2:ℝ) (3/2)) :
       |Real.log c| ≤ Real.log 2 := by
   …

5. lemma OAI.HarmonicCounterexample.LinearODE.undo_scalar_normalization line 89

   Source documentation

   Undoing exactly the scalar baseline normalizer preserves an exact positive scalar-permutation endpoint and adds only the genuine baseline integral to its logarithm. This is an equality of actual operators, not a weighted model.

   lemma undo_scalar_normalization {R : Type*} [NormedAddCommGroup R] [NormedSpace ℝ R]
       {Y perm : R} {I c : ℝ} (he : Real.exp (-I) • Y=c • perm) :
       Y=(Real.exp I*c) • perm := by
   …

6. lemma OAI.HarmonicCounterexample.LinearODE.lifted_target_log line 96
7. theorem OAI.HarmonicCounterexample.LinearODE.actual_baseline_log_cost line 106

   Source documentation

   Actual scalar PB baseline integrated log cost. The constant precedes all pulse histories and lengths; no value of an unproved scalar ODE is supplied.

   theorem actual_baseline_log_cost {α p : ℝ → ℝ}
       (hα : Continuous α) (hp : Continuous p)
       {M Mp B β p₀ θ γ δ T : ℝ}
       (hM : 0 ≤ M) (hMp : 0 ≤ Mp) (hθ : 0 ≤ θ) (hγ : 0 < γ)
       (hδ : 0 ≤ δ) (hT : 0 ≤ T)
       (hαn : ∀ t,|α t| ≤ M) (hpn : ∀ t,|p t| ≤ Mp)
       (hAp : ∀ t,0 ≤ t → 0 ≤ α t*B) (hroot : β*B-p₀*θ-θ^2=0)
       (hscale : ∀ t ∈ Icc 0 T,|α t-β| ≤ δ)
       (hpt : ∀ t ∈ Icc 0 T,|p t-p₀| ≤ δ)
       (hpl : ∀ t ∈ Icc 0 T,γ ≤ p t) :
       |∫ t in (0:ℝ)..T,scalarBaseline (fun s => α s*B) p θ t| ≤
         (θ+((|B|+|θ|)/γ)*δ)*T := by
   …

   Mentions: OAI.HarmonicCounterexample.LinearODE.scalarBaseline

8. lemma OAI.HarmonicCounterexample.LinearODE.bergerSlowGenerator_eq_smul line 153
9. theorem OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitBergerPacket_selected line 179

   Source documentation

   Exact representation of the normalized smooth finite-word coefficient and its time derivative by the selected Berger angular generator.

   theorem unitBergerPacket_selected (a : Fin n → ℝ) (D : Fin n → R)
       (r B β p₀ θ : ℝ) (d : ℝ → Fin n)
       (hd : ∀ t i,i ≠ d t → bump i t=0 ∧ deriv (bump i) t=0) (t : ℝ) :
       unitPacketCoefficient a (fun j => bergerSlowGenerator r B β p₀ θ 1 (D j)) t=
         bergerSlowGenerator r B β p₀ θ (unitPacketScalar a t) (D (d (duration n*t))) ∧
       unitPacketCoefficientD a (fun j => bergerSlowGenerator r B β p₀ θ 1 (D j)) t=
         bergerSlowGenerator r B β p₀ θ (unitPacketScalarD a t) (D (d (duration n*t))) := by
   …

   Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.bump, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketCoefficient, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketScalar, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.duration, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketCoefficientD, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketScalarD

10. theorem OAI.HarmonicCounterexample.FiniteControl.SmoothWord.exists_unit_round_gap_selector line 193

    Source documentation

    The normalized selector is locally constant unless every actual scalar packet vanishes on a neighborhood. Thus angular changes occur on ROUND gaps.

    theorem exists_unit_round_gap_selector (n : ℕ) [NeZero n] :
        ∃ d : ℝ → Fin n,
          (∀ t i,i ≠ d t → bump i (duration n*t)=0 ∧ deriv (bump i) (duration n*t)=0) ∧
          ∀ t,(∀ᶠ s in 𝓝 t,d s=d t) ∨
            (∀ᶠ s in 𝓝 t,∀ a : Fin n → ℝ,unitPacketScalar a s=0) := by
    …

    Mentions: OAI.HarmonicCounterexample.FiniteControl.SmoothWord.bump, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.duration, OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketScalar

11. theorem OAI.HarmonicCounterexample.LinearODE.actual_finite_berger_word_estimates line 244

    Source documentation

    Model-specific value and variational-slope estimates for an EXPLICIT smooth finite word, with all shape identities and bounds discharged. The selector and constants are chosen before every history, amplitude vector and duration.

    theorem actual_finite_berger_word_estimates (basis : OrthonormalBasis ι ℝ E)
        (r B β p₀ θ γ : ℝ) (D : Fin n → E →L[ℝ] E) {M U : ℝ}
        (hM : 0 ≤ M) (hU : 0 ≤ U) (hθ : 0 ≤ θ) (hγ : 0 < γ)
        (hc : p₀+2*θ ≠ 0) (hroot : β*B-p₀*θ-θ^2=0) :
        ∃ Z C : ℝ,∃ d : ℝ → Fin n,0 ≤ Z ∧ 1 ≤ C ∧
          (∀ t,(∀ᶠ s in 𝓝 t,d s=d t) ∨
            (∀ᶠ s in 𝓝 t,∀ v : Fin n → ℝ,unitPacketScalar v s=0)) ∧ ∀ (A : H → ℝ → E →L[ℝ] E) (b : ℝ → ℝ)
          (B' : H → ℝ → H →L[ℝ] OperatorPhase E →L[ℝ] OperatorPhase E)
          (A' : H → ℝ → H →L[ℝ] E →L[ℝ] E) (x h : H)
          (α p : ℝ → ℝ) (amps rays : Fin n → ℝ) (Mp MB MA Mb l B₀ a T δ ε : ℝ),
          (∀ j,|amps j| ≤ U) → (∀ j,|rays j| ≤ U) →
          Continuous (A x) → Continuous b → Continuous (B' x) →
    …

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

12. theorem OAI.HarmonicCounterexample.LinearODE.actual_slope_jet_continuousOn line 367

    Source documentation

    The regular Riccati value and its entire Frechet jet are continuous in physical time on the actual nonnegative half-line. Invertibility is produced from positivity, not assumed as an analytic bridge.

    theorem actual_slope_jet_continuousOn
        (A : H → ℝ → E →L[ℝ] E) (b : ℝ → ℝ)
        (B' : H → ℝ → H →L[ℝ] OperatorPhase E →L[ℝ] OperatorPhase E)
        (A' : H → ℝ → H →L[ℝ] E →L[ℝ] E) (p : 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)
        (hpos : ∀ t v,0 ≤ inner ℝ v (A p t v)) {l : ℝ} (hl : 0 < l) :
        ContinuousOn (slope (A p) b l) (Ici 0) ∧
        ContinuousOn (slopeJet A b B' l p) (Ici 0) := by
    …

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

13. theorem OAI.HarmonicCounterexample.LinearODE.actual_normalized_slope_hasFDerivAt line 391

    Source documentation

    The normalized coefficient's first jet is the genuine parameter derivative of the actual center-regular PB slope after slow-time rescaling.

    theorem actual_normalized_slope_hasFDerivAt
        (A : H → ℝ → E →L[ℝ] E) (b v : ℝ → ℝ)
        (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 MA Mb : ℝ} (hM : 0 ≤ M) (hMA : 0 ≤ MA) (hMb : 0 ≤ Mb)
        (hnB : ∀ p ∈ S,∀ t,‖block (leftAction (A p)) b t‖ ≤ M)
        (hnB' : ∀ p ∈ S,∀ t,‖B' p t‖ ≤ M)
        (hnA : ∀ p ∈ S,∀ t,‖A p t‖ ≤ MA) (hnb : ∀ t,|b t| ≤ Mb)
        (hpos : ∀ p ∈ S,∀ t w,0 ≤ inner ℝ w (A p t w)) {l : ℝ} (hl : 0 < l)
        {p : H} (hp : p ∈ S) {a T u : ℝ} (ha : 0 ≤ a) (hT : 0 ≤ T) (hu : 0 ≤ u) :
    …

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

14. theorem OAI.HarmonicCounterexample.LinearODE.integral_gronwall line 430

    Source documentation

    The variable-coefficient Gronwall estimate in precisely the integrated norm used for long pulses. No supremum-times-pulse-length loss occurs.

    theorem integral_gronwall {a b c : ℝ} (hab : a ≤ b)
        (u q r : ℝ → ℝ) (hu : Continuous u) (hq : Continuous q) (hr : Continuous r)
        (hq0 : ∀ t ∈ Icc a b,0 ≤ q t) (hr0 : ∀ t ∈ Icc a b,0 ≤ r t)
        (hineq : ∀ t ∈ Icc a b,u t ≤ c+∫ s in a..t,q s*u s+r s) :
        u b ≤ (c+∫ s in a..b,r s)*Real.exp (∫ s in a..b,q s) := by
    …

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

15. theorem OAI.HarmonicCounterexample.LinearODE.norm_le_integrated_gronwall line 475

    Source documentation

    Sharp-in-L1 stability for a genuinely differentiable Banach-valued path.

    theorem norm_le_integrated_gronwall {a b : ℝ} (hab : a ≤ b)
        (f f' : ℝ → E) (hf : ∀ t,HasDerivAt f (f' t) t) (hfc : Continuous f')
        (q r : ℝ → ℝ) (hq : Continuous q) (hr : Continuous r)
        (hq0 : ∀ t ∈ Icc a b,0 ≤ q t) (hr0 : ∀ t ∈ Icc a b,0 ≤ r t)
        (hbound : ∀ t ∈ Icc a b,‖f' t‖ ≤ q t*‖f t‖+r t) :
        ‖f b‖ ≤ (‖f a‖+∫ s in a..b,r s)*Real.exp (∫ s in a..b,q s) := by
    …

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

16. lemma OAI.HarmonicCounterexample.LinearODE.flow_norm_integral_bound line 517

    Source documentation

    The actual Peano--Baker flow has the sharp L1 exponential bound.

    lemma flow_norm_integral_bound {A : ℝ → E →L[ℝ] E} (hA : Continuous A)
        {M : ℝ} (hM : 0 ≤ M) (hbound : ∀ t,‖A t‖ ≤ M) (x : E) {t : ℝ} (ht : 0 ≤ t) :
        ‖flow A x t‖ ≤ ‖x‖*Real.exp (∫ s in (0:ℝ)..t,‖A s‖) := by
    …

    Mentions: OAI.HarmonicCounterexample.LinearODE.flow

17. lemma OAI.HarmonicCounterexample.LinearODE.norm_integral_mono_upper line 528
18. theorem OAI.HarmonicCounterexample.LinearODE.flow_L1_difference line 538

    Source documentation

    Actual solution stability with a length-independent L1 coefficient error. Both solutions are constructed, not postulated, and no commutativity is used.

    theorem flow_L1_difference {A B : ℝ → E →L[ℝ] E}
        (hA : Continuous A) (hB : Continuous B) {MA MB : ℝ} (hMA : 0 ≤ MA) (hMB : 0 ≤ MB)
        (hAb : ∀ s,‖A s‖ ≤ MA) (hBb : ∀ s,‖B s‖ ≤ MB) (x : E) {t : ℝ} (ht : 0 ≤ t) :
        ‖flow A x t-flow B x t‖ ≤
          ‖x‖*Real.exp ((∫ s in (0:ℝ)..t,‖A s‖)+(∫ s in (0:ℝ)..t,‖B s‖)) *
            (∫ s in (0:ℝ)..t,‖A s-B s‖) := by
    …

    Mentions: OAI.HarmonicCounterexample.LinearODE.flow

19. def OAI.HarmonicCounterexample.LinearODE.jetBlock line 592

    Source documentation

    The exact first-jet coefficient on value/parameter-derivative pairs.

    def jetBlock (A : E →L[ℝ] E) (A' : H →L[ℝ] E →L[ℝ] E) :
        E×(H →L[ℝ] E) →L[ℝ] E×(H →L[ℝ] E) :=
    …

20. lemma OAI.HarmonicCounterexample.LinearODE.jetBlock_apply line 599
21. lemma OAI.HarmonicCounterexample.LinearODE.jetBlock_continuous line 603
22. lemma OAI.HarmonicCounterexample.LinearODE.jetBlock_norm line 613
23. lemma OAI.HarmonicCounterexample.LinearODE.jetBlock_sub line 636
24. lemma OAI.HarmonicCounterexample.LinearODE.flow_jet line 650

    Source documentation

    The actual parameter jet is itself the actual constructed linear flow.

    lemma flow_jet (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 : ℝ) :
        (flow (A p) x t,flowD A A' x p t) =
          flow (fun s => jetBlock (A p s) (A' p s)) (x,0) t := by
    …

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

25. theorem OAI.HarmonicCounterexample.LinearODE.flow_jet_L1_difference line 669

    Source documentation

    A genuine C1-in-parameter endpoint estimate, with an L1 (not duration) constant, for two actual coefficient families.

    theorem flow_jet_L1_difference
        (A B : H → ℝ → E →L[ℝ] E) (A' B' : H → ℝ → H →L[ℝ] E →L[ℝ] E)
        (hA : ∀ p,Continuous (A p)) (hB : ∀ p,Continuous (B p))
        (hA' : ∀ p,Continuous (A' p)) (hB' : ∀ p,Continuous (B' p))
        {M : ℝ} (hM : 0 ≤ M) (hbA : ∀ p s,‖A p s‖ ≤ M) (hbB : ∀ p s,‖B p s‖ ≤ M)
        (hbA' : ∀ p s,‖A' p s‖ ≤ M) (hbB' : ∀ p s,‖B' p s‖ ≤ M)
        (x : E) (p : H) {t : ℝ} (ht : 0 ≤ t) :
        max ‖flow (A p) x t-flow (B p) x t‖ ‖flowD A A' x p t-flowD B B' x p t‖ ≤
          ‖x‖*Real.exp ((∫ s in (0:ℝ)..t,‖jetBlock (A p s) (A' p s)‖)+
            (∫ s in (0:ℝ)..t,‖jetBlock (B p s) (B' p s)‖)) *
            (∫ s in (0:ℝ)..t,‖jetBlock (A p s-B p s) (A' p s-B' p s)‖) := by
    …

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

26. lemma OAI.HarmonicCounterexample.LinearODE.flowD_hasDerivAt_pointwise line 714

    Source documentation

    The actual time variational equation needs bounds only at the current parameter, not at the irrelevant parameters outside the admissible ball.

    lemma flowD_hasDerivAt_pointwise
        (A : H → ℝ → E →L[ℝ] E) (A' : H → ℝ → H →L[ℝ] E →L[ℝ] E)
        (p : H) (hA : Continuous (A p)) (hA' : Continuous (A' p))
        {M : ℝ} (hM : 0 ≤ M) (hb : ∀ s,‖A p s‖ ≤ M) (hb' : ∀ s,‖A' p s‖ ≤ M)
        (x : E) (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

27. theorem OAI.HarmonicCounterexample.LinearODE.flow_jet_L1_difference_pointwise line 729

    Source documentation

    Local-in-parameter actual jet stability. The parameter universe is not silently restricted; coefficients outside the admissible set are unused.

    theorem flow_jet_L1_difference_pointwise
        (A B : H → ℝ → E →L[ℝ] E) (A' B' : H → ℝ → H →L[ℝ] E →L[ℝ] E)
        (p : H) (hA : Continuous (A p)) (hB : Continuous (B p))
        (hA' : Continuous (A' p)) (hB' : Continuous (B' p))
        {M : ℝ} (hM : 0 ≤ M) (hbA : ∀ s,‖A p s‖ ≤ M) (hbB : ∀ s,‖B p s‖ ≤ M)
        (hbA' : ∀ s,‖A' p s‖ ≤ M) (hbB' : ∀ s,‖B' p s‖ ≤ M)
        (x : E) {t : ℝ} (ht : 0 ≤ t) :
        max ‖flow (A p) x t-flow (B p) x t‖ ‖flowD A A' x p t-flowD B B' x p t‖ ≤
          ‖x‖*Real.exp ((∫ s in (0:ℝ)..t,‖jetBlock (A p s) (A' p s)‖)+
            (∫ s in (0:ℝ)..t,‖jetBlock (B p s) (B' p s)‖)) *
            (∫ s in (0:ℝ)..t,‖jetBlock (A p s-B p s) (A' p s-B' p s)‖) := by
    …

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

28. theorem OAI.HarmonicCounterexample.LinearODE.flow_fderiv_L1_difference_on line 748

    Source documentation

    Quantitative C1 endpoint stability for the genuine Frechet derivatives on an admissible open connected parameter domain. The right side depends on L1 coefficient and jet norms, so it does not lose a factor equal to pulse duration.

    theorem flow_fderiv_L1_difference_on
        (A B : H → ℝ → E →L[ℝ] E) (A' B' : H → ℝ → H →L[ℝ] E →L[ℝ] E)
        {S : Set H} (hS : IsOpen S) (hSc : IsPreconnected S)
        (hA : ∀ p ∈ S,Continuous (A p)) (hB : ∀ p ∈ S,Continuous (B p))
        (hA' : ∀ p ∈ S,Continuous (A' p)) (hB' : ∀ p ∈ S,Continuous (B' p))
        (hdA : ∀ p ∈ S,∀ t,HasFDerivAt (fun q => A q t) (A' p t) p)
        (hdB : ∀ p ∈ S,∀ t,HasFDerivAt (fun q => B q t) (B' p t) p)
        {M : ℝ} (hM : 0 ≤ M) (hbA : ∀ p ∈ S,∀ s,‖A p s‖ ≤ M)
        (hbB : ∀ p ∈ S,∀ s,‖B p s‖ ≤ M) (hbA' : ∀ p ∈ S,∀ s,‖A' p s‖ ≤ M)
        (hbB' : ∀ p ∈ S,∀ s,‖B' p s‖ ≤ M)
        (x : E) {p : H} (hp : p ∈ S) {t : ℝ} (ht : 0 ≤ t) :
        max ‖flow (A p) x t-flow (B p) x t‖
    …

    Mentions: OAI.HarmonicCounterexample.LinearODE.flow

29. lemma OAI.HarmonicCounterexample.LinearODE.slow_time_integral_norm line 791

    Source documentation

    Rescaling an integrated error introduces NO pulse-duration factor.

    lemma slow_time_integral_norm {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
        (X : ℝ → F) (a : ℝ) {T : ℝ} (hT : 0 < T) :
        (∫ τ in (0:ℝ)..1,‖T • X (a+T*τ)‖)=(∫ t in a..a+T,‖X t‖) := by
    …

    Mentions: OAI.HarmonicCounterexample.a

30. lemma OAI.HarmonicCounterexample.LinearODE.jetBlock_integral_le line 803
31. theorem OAI.HarmonicCounterexample.LinearODE.pulse_endpoint_C1_of_integrated_errors line 821

    Source documentation

    The actual flow AND its genuine parameter Frechet derivative converge in C1 from integrated coefficient errors. All resulting constants are independent of the (possibly large) global M used only to construct/differentiate PB flow.

    theorem pulse_endpoint_C1_of_integrated_errors
        (A B : H → ℝ → E →L[ℝ] E) (A' B' : H → ℝ → H →L[ℝ] E →L[ℝ] E)
        {S : Set H} (hS : IsOpen S) (hSc : IsPreconnected S)
        (hA : ∀ p ∈ S,Continuous (A p)) (hB : ∀ p ∈ S,Continuous (B p))
        (hA' : ∀ p ∈ S,Continuous (A' p)) (hB' : ∀ p ∈ S,Continuous (B' p))
        (hdA : ∀ p ∈ S,∀ t,HasFDerivAt (fun q => A q t) (A' p t) p)
        (hdB : ∀ p ∈ S,∀ t,HasFDerivAt (fun q => B q t) (B' p t) p)
        {M : ℝ} (hM : 0 ≤ M) (hbA : ∀ p ∈ S,∀ s,‖A p s‖ ≤ M)
        (hbB : ∀ p ∈ S,∀ s,‖B p s‖ ≤ M) (hbA' : ∀ p ∈ S,∀ s,‖A' p s‖ ≤ M)
        (hbB' : ∀ p ∈ S,∀ s,‖B' p s‖ ≤ M)
        (x : E) {p : H} (hp : p ∈ S) {C η : ℝ}
        (hIB : (∫ s in (0:ℝ)..1,‖B p s‖)+(∫ s in (0:ℝ)..1,‖B' p s‖) ≤ C)
    …

32. lemma OAI.HarmonicCounterexample.LinearODE.opNorm_le_sum_basis line 895

    Source documentation

    Finite-direction estimates control the genuine derivative operator norm. No interchange of supremum and integral is used.

    lemma opNorm_le_sum_basis (b : OrthonormalBasis ι ℝ H) (L : H →L[ℝ] F) :
        ‖L‖ ≤ ∑ i,‖L (b i)‖ := by
    …

    Mentions: OAI.HarmonicCounterexample.b

33. theorem OAI.HarmonicCounterexample.LinearODE.integrated_opNorm_le_basis_sum line 915

    Source documentation

    Turning the integrated raywise Riccati-jet estimates into the C1 operator estimate costs only the FIXED parameter dimension, never the pulse duration.

    theorem integrated_opNorm_le_basis_sum (b : OrthonormalBasis ι ℝ H)
        {L : ℝ → H →L[ℝ] F} {a z C : ℝ} (haz : a ≤ z)
        (hL : ContinuousOn L (Set.Icc a z))
        (hI : ∀ i,(∫ t in a..z,‖L t (b i)‖) ≤ C) :
        (∫ t in a..z,‖L t‖) ≤ (Fintype.card ι:ℝ)*C := by
    …

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

34. theorem OAI.HarmonicCounterexample.LinearODE.endpoint_C1_of_matrix_ray_errors line 959

    Source documentation

    Passage from finite Frobenius estimates on the actual Riccati value and parameter basis rays to the genuine C1 endpoint estimate. The parameter and angular coordinate constants are fixed before every history map.

    theorem endpoint_C1_of_matrix_ray_errors
        (e : OrthonormalBasis ι ℝ E) (h : OrthonormalBasis κ ℝ H)
        {C : ℝ} (hC : 0 ≤ C) :
        ∃ J : ℝ,C ≤ J ∧ 0 ≤ J ∧
        ∀ (A B : H → ℝ → E →L[ℝ] E) (A' B' : H → ℝ → H →L[ℝ] E →L[ℝ] E)
          (S : Set H) (p : H) (M η : ℝ) (x : E),
          IsOpen S → IsPreconnected S → p ∈ S →
          (∀ q ∈ S,Continuous (A q)) → (∀ q ∈ S,Continuous (B q)) →
          (∀ q ∈ S,Continuous (A' q)) → (∀ q ∈ S,Continuous (B' q)) →
          (∀ q ∈ S,∀ t,HasFDerivAt (fun r => A r t) (A' q t) q) →
          (∀ q ∈ S,∀ t,HasFDerivAt (fun r => B r t) (B' q t) q) →
          0 ≤ M → 0 ≤ η →
    …

35. theorem OAI.HarmonicCounterexample.LinearODE.pulse_endpoint_C1_of_contracted_errors line 1031

    Source documentation

    A fixed contraction lifts value and genuine parameter derivative L1 errors to the endpoint flow, without a dimension- or duration-dependent loss. Taking L to be left multiplication gives the actual operator endpoint.

    theorem pulse_endpoint_C1_of_contracted_errors
        (L : V →L[ℝ] E →L[ℝ] E) (hL : ‖L‖ ≤ 1)
        (A B : H → ℝ → V) (A' B' : H → ℝ → H →L[ℝ] V)
        {S : Set H} (hS : IsOpen S) (hSc : IsPreconnected S)
        (hA : ∀ p ∈ S,Continuous (A p)) (hB : ∀ p ∈ S,Continuous (B p))
        (hA' : ∀ p ∈ S,Continuous (A' p)) (hB' : ∀ p ∈ S,Continuous (B' p))
        (hdA : ∀ p ∈ S,∀ t,HasFDerivAt (fun q => A q t) (A' p t) p)
        (hdB : ∀ p ∈ S,∀ t,HasFDerivAt (fun q => B q t) (B' p t) p)
        {M : ℝ} (hM : 0 ≤ M) (hbA : ∀ p ∈ S,∀ s,‖A p s‖ ≤ M)
        (hbB : ∀ p ∈ S,∀ s,‖B p s‖ ≤ M) (hbA' : ∀ p ∈ S,∀ s,‖A' p s‖ ≤ M)
        (hbB' : ∀ p ∈ S,∀ s,‖B' p s‖ ≤ M)
        (x : E) {p : H} (hp : p ∈ S) {C η : ℝ}
    …

36. theorem OAI.HarmonicCounterexample.LinearODE.contracted_endpoint_C1_of_matrix_ray_errors line 1106

    Source documentation

    Passage from finite Frobenius estimates on the actual Riccati value and parameter basis rays to the genuine C1 endpoint estimate. The parameter and angular coordinate constants are fixed before every history map.

    theorem contracted_endpoint_C1_of_matrix_ray_errors
        (L : (E →L[ℝ] E) →L[ℝ] F →L[ℝ] F) (hL : ‖L‖ ≤ 1)
        (e : OrthonormalBasis ι ℝ E) (h : OrthonormalBasis κ ℝ H)
        {C : ℝ} (hC : 0 ≤ C) :
        ∃ J : ℝ,C ≤ J ∧ 0 ≤ J ∧
        ∀ (A B : H → ℝ → E →L[ℝ] E) (A' B' : H → ℝ → H →L[ℝ] E →L[ℝ] E)
          (S : Set H) (p : H) (M η : ℝ) (x : F),
          IsOpen S → IsPreconnected S → p ∈ S →
          (∀ q ∈ S,Continuous (A q)) → (∀ q ∈ S,Continuous (B q)) →
          (∀ q ∈ S,Continuous (A' q)) → (∀ q ∈ S,Continuous (B' q)) →
          (∀ q ∈ S,∀ t,HasFDerivAt (fun r => A r t) (A' q t) q) →
          (∀ q ∈ S,∀ t,HasFDerivAt (fun r => B r t) (B' q t) q) →
    …

37. theorem OAI.HarmonicCounterexample.LinearODE.operator_endpoint_C1_of_matrix_ray_errors line 1181

    Source documentation

    Passage from finite Frobenius estimates on the actual Riccati value and parameter basis rays to the genuine C1 endpoint estimate. The parameter and angular coordinate constants are fixed before every history map.

    theorem operator_endpoint_C1_of_matrix_ray_errors
        (e : OrthonormalBasis ι ℝ E) (h : OrthonormalBasis κ ℝ H)
        {C : ℝ} (hC : 0 ≤ C) :
        ∃ J : ℝ,C ≤ J ∧ 0 ≤ J ∧
        ∀ (A B : H → ℝ → E →L[ℝ] E) (A' B' : H → ℝ → H →L[ℝ] E →L[ℝ] E)
          (S : Set H) (p : H) (M η : ℝ),
          IsOpen S → IsPreconnected S → p ∈ S →
          (∀ q ∈ S,Continuous (A q)) → (∀ q ∈ S,Continuous (B q)) →
          (∀ q ∈ S,Continuous (A' q)) → (∀ q ∈ S,Continuous (B' q)) →
          (∀ q ∈ S,∀ t,HasFDerivAt (fun r => A r t) (A' q t) q) →
          (∀ q ∈ S,∀ t,HasFDerivAt (fun r => B r t) (B' q t) q) →
          0 ≤ M → 0 ≤ η →
    …

38. def OAI.HarmonicCounterexample.LinearODE.clip01 line 1233

    Source documentation

    Exterior extension is by constant coefficients, never by altering the actual solution on the pulse.

    def clip01 (t : ℝ) : ℝ := min 1 (max 0 t)

39. lemma OAI.HarmonicCounterexample.LinearODE.clip01_continuous line 1234
40. lemma OAI.HarmonicCounterexample.LinearODE.clip01_mem line 1236
41. lemma OAI.HarmonicCounterexample.LinearODE.clip01_eq line 1238
42. lemma OAI.HarmonicCounterexample.LinearODE.integral_clip01 line 1240
43. theorem OAI.HarmonicCounterexample.LinearODE.clipped_operator_endpoint_C1_of_matrix_ray_errors line 1273

    Source documentation

    Passage from finite Frobenius estimates on the actual Riccati value and parameter basis rays to the genuine C1 endpoint estimate. The parameter and angular coordinate constants are fixed before every history map.

    theorem clipped_operator_endpoint_C1_of_matrix_ray_errors
        (e : OrthonormalBasis ι ℝ E) (h : OrthonormalBasis κ ℝ H)
        {C : ℝ} (hC : 0 ≤ C) :
        ∃ J : ℝ,C ≤ J ∧ 0 ≤ J ∧
        ∀ (A B : H → ℝ → E →L[ℝ] E) (A' B' : H → ℝ → H →L[ℝ] E →L[ℝ] E)
          (S : Set H) (p : H) (M η : ℝ),
          IsOpen S → IsPreconnected S → p ∈ S →
          (∀ q ∈ S,ContinuousOn (A q) (Set.Icc (0:ℝ) 1)) → (∀ q ∈ S,ContinuousOn (B q) (Set.Icc (0:ℝ) 1)) →
          (∀ q ∈ S,ContinuousOn (A' q) (Set.Icc (0:ℝ) 1)) → (∀ q ∈ S,ContinuousOn (B' q) (Set.Icc (0:ℝ) 1)) →
          (∀ q ∈ S,∀ t ∈ Set.Icc (0:ℝ) 1,HasFDerivAt (fun r => A r t) (A' q t) q) →
          (∀ q ∈ S,∀ t ∈ Set.Icc (0:ℝ) 1,HasFDerivAt (fun r => B r t) (B' q t) q) →
          0 ≤ M → 0 ≤ η →
    …

44. lemma OAI.HarmonicCounterexample.LinearODE.term_congr_interval line 1338

    Source documentation

    PB iteration uses only coefficient values on the actual elapsed interval.

    lemma term_congr_interval {A B : ℝ → E →L[ℝ] E} {b : ℝ}
        (hAB : EqOn A B (Icc 0 b)) (x : E) (n : ℕ) :
        ∀ t ∈ Icc 0 b,term A x n t=term B x n t := by
    …

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

45. lemma OAI.HarmonicCounterexample.LinearODE.flow_congr_interval line 1355

    Source documentation

    Exact identity, not an endpoint estimate, under exterior coefficient extension; this also identifies genuine parameter derivatives by congruence.

    lemma flow_congr_interval {A B : ℝ → E →L[ℝ] E} {b : ℝ}
        (hAB : EqOn A B (Icc 0 b)) (x : E) {t : ℝ} (ht : t ∈ Icc 0 b) :
        flow A x t=flow B x t := by
    …

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

46. lemma OAI.HarmonicCounterexample.LinearODE.flow_clip01_endpoint line 1363
47. lemma OAI.HarmonicCounterexample.LinearODE.normalized_matrix_integral line 1369

    Source documentation

    The Frobenius integrated error of the normalized coefficient is EXACTLY that of the actual physical-time Riccati comparison. No factor T is lost.

    lemma normalized_matrix_integral {F G : Type*} [NormedAddCommGroup F]
        [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G]
        (L : F →L[ℝ] G) (P S : ℝ → F) (v : ℝ → ℝ) (I : F) (a : ℝ) {T : ℝ} (hT : 0 < T) :
        (∫ u in (0:ℝ)..1,‖L (T • (P (a+T*u)-v (a+T*u) • I))-L (S u)‖)=
        ∫ t in a..a+T,‖L (P t)-L (v t • I+T⁻¹ • S (T⁻¹*(t-a)))‖ := by
    …

    Mentions: OAI.HarmonicCounterexample.a

48. lemma OAI.HarmonicCounterexample.LinearODE.term_history_eq line 1412

    Source documentation

    Peano--Baker construction is causal on the positive half line, before any existence/summability assumption is imposed.

    lemma term_history_eq {A B : ℝ → E →L[ℝ] E} {T : ℝ}
        (h : Set.EqOn A B (Set.Icc 0 T)) (x : E) (n : ℕ) :
        Set.EqOn (term A x n) (term B x n) (Set.Icc 0 T) := by
    …

    Mentions: OAI.HarmonicCounterexample.LinearODE.term

49. lemma OAI.HarmonicCounterexample.LinearODE.flow_history_eq line 1428
50. lemma OAI.HarmonicCounterexample.LinearODE.termD_history_zero line 1437

    Source documentation

    A control parameter not used in the incoming history has identically zero actual variational flow throughout that history.

    lemma termD_history_zero {A : H → ℝ → E →L[ℝ] E}
        {A' : H → ℝ → H →L[ℝ] E →L[ℝ] E} {p : H} {T : ℝ}
        (h : ∀ t ∈ Set.Icc 0 T,A' p t=0) (x : E) (n : ℕ) :
        ∀ t ∈ Set.Icc 0 T,termD A A' x p n t=0 := by
    …

    Mentions: OAI.HarmonicCounterexample.LinearODE.termD

51. lemma OAI.HarmonicCounterexample.LinearODE.flowD_history_zero line 1458
52. lemma OAI.HarmonicCounterexample.LinearODE.solution_unique_on_Icc line 1469

    Source documentation

    Exact restart, independent of earlier coefficients, follows from interval ODE uniqueness with the actual incoming value, not an artificially reset value.

    lemma solution_unique_on_Icc {A : ℝ → E →L[ℝ] E} {M a b : ℝ}
        (hM : 0 ≤ M) (hb : ∀ t ∈ Set.Ico a b,‖A t‖ ≤ M) {f g : ℝ → E}
        (hfc : ContinuousOn f (Set.Icc a b)) (hgc : ContinuousOn g (Set.Icc a b))
        (hf : ∀ t ∈ Set.Ico a b,HasDerivAt f (A t (f t)) t)
        (hg : ∀ t ∈ Set.Ico a b,HasDerivAt g (A t (g t)) t)
        (he : f a=g a) : Set.EqOn f g (Set.Icc a b) := by
    …

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

53. def OAI.HarmonicCounterexample.LinearODE.scalarNormalized line 1499
54. lemma OAI.HarmonicCounterexample.LinearODE.scalarNormalized_deriv line 1505

    Source documentation

    Removing the exact scalar baseline, rather than its frozen limit, from an actual solution is an exact differentiable identity.

    lemma scalarNormalized_deriv {v : ℝ → ℝ} (hv : Continuous v)
        {P : ℝ → E →L[ℝ] E} {f : ℝ → E} {a t : ℝ}
        (hf : HasDerivAt f (P t (f t)) t) :
        HasDerivAt (scalarNormalized v a f)
          ((P t-v t • ContinuousLinearMap.id ℝ E) (scalarNormalized v a f t)) t := by
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.LinearODE.scalarNormalized

55. lemma OAI.HarmonicCounterexample.LinearODE.scalarNormalized_initial line 1520
56. lemma OAI.HarmonicCounterexample.LinearODE.scalarNormalized_rescaled_deriv line 1526

    Source documentation

    Exact passage to slow pulse time. The factor T belongs inside the coefficient; scalar phase may grow with T but causes no error amplification.

    lemma scalarNormalized_rescaled_deriv {v : ℝ → ℝ} (hv : Continuous v)
        {P : ℝ → E →L[ℝ] E} {f : ℝ → E} {a T τ : ℝ}
        (hf : HasDerivAt f (P (a+T*τ) (f (a+T*τ))) (a+T*τ)) :
        HasDerivAt (fun u => scalarNormalized v a f (a+T*u))
          ((T • (P (a+T*τ)-v (a+T*τ) • ContinuousLinearMap.id ℝ E))
            (scalarNormalized v a f (a+T*τ))) τ := by
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.LinearODE.scalarNormalized

57. theorem OAI.HarmonicCounterexample.LinearODE.scalarNormalized_eq_flow line 1539

    Source documentation

    The normalized ACTUAL solution equals the actual constructed first-order flow on the entire pulse. The incoming value is not replaced or estimated.

    theorem scalarNormalized_eq_flow {v : ℝ → ℝ} (hv : Continuous v)
        {P : ℝ → E →L[ℝ] E} {f : ℝ → E} {a T : ℝ}
        (hf : ∀ t,HasDerivAt f (P t (f t)) t)
        {C : ℝ → E →L[ℝ] E}
        (hC : Continuous C) {M : ℝ} (hM : 0 ≤ M) (hCb : ∀ t,‖C t‖ ≤ M)
        (hCe : ∀ τ ∈ Set.Icc (0:ℝ) 1,
          C τ=T • (P (a+T*τ)-v (a+T*τ) • ContinuousLinearMap.id ℝ E)) :
        ∀ τ ∈ Set.Icc (0:ℝ) 1,
          scalarNormalized v a f (a+T*τ)=flow C (f a) τ := by
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.LinearODE.scalarNormalized, OAI.HarmonicCounterexample.LinearODE.flow

58. lemma OAI.HarmonicCounterexample.LinearODE.scalarNormalized_hasFDerivAt_parameter line 1559

    Source documentation

    The scalar baseline is independent of the current control parameter, so normalization commutes exactly with its Frechet derivative.

    lemma scalarNormalized_hasFDerivAt_parameter {H : Type*}
        [NormedAddCommGroup H] [NormedSpace ℝ H]
        {f : H → ℝ → E} {f' : H →L[ℝ] E} {p : H} {v : ℝ → ℝ} {a t : ℝ}
        (hf : HasFDerivAt (fun q => f q t) f' p) :
        HasFDerivAt (fun q => scalarNormalized v a (f q) t)
          (Real.exp (-(∫ s in a..t,v s)) • f') p := hf.const_smul _
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.LinearODE.scalarNormalized

59. lemma OAI.HarmonicCounterexample.LinearODE.scalarNormalized_deriv_local line 1589

    Source documentation

    Local normalization: only integrability from a to t and continuity at t are required of the scalar baseline. Irrelevant pre-pulse poles are allowed.

    lemma scalarNormalized_deriv_local {v : ℝ → ℝ} {a t : ℝ}
        (hvint : IntervalIntegrable v volume a t) (hvmeas : StronglyMeasurableAtFilter v (𝓝 t))
        (hv : ContinuousAt v t) {P : ℝ → E →L[ℝ] E} {f : ℝ → E}
        (hf : HasDerivAt f (P t (f t)) t) :
        HasDerivAt (scalarNormalized v a f)
          ((P t-v t • ContinuousLinearMap.id ℝ E) (scalarNormalized v a f t)) t := by
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.LinearODE.scalarNormalized

60. lemma OAI.HarmonicCounterexample.LinearODE.scalarNormalized_rescaled_deriv_local line 1602
61. theorem OAI.HarmonicCounterexample.LinearODE.scalarNormalized_eq_flow_on line 1618

    Source documentation

    Exact identification of the normalized actual solution with PB flow, using derivatives only on the pulse. The exterior extension is applied only to its coefficient, never to the unknown solution or its derivative.

    theorem scalarNormalized_eq_flow_on {v : ℝ → ℝ} {a T : ℝ}
        (hT : 0 ≤ T) (hvc : ∀ t ∈ Icc a (a+T),ContinuousAt v t)
        (hvm : StronglyMeasurable v)
        {P : ℝ → E →L[ℝ] E} {f : ℝ → E}
        (hf : ∀ t ∈ Icc a (a+T),HasDerivAt f (P t (f t)) t)
        {C : ℝ → E →L[ℝ] E}
        (hC : Continuous C) {M : ℝ} (hM : 0 ≤ M) (hCb : ∀ t,‖C t‖ ≤ M)
        (hCe : ∀ τ ∈ Icc (0:ℝ) 1,
          C τ=T • (P (a+T*τ)-v (a+T*τ) • ContinuousLinearMap.id ℝ E)) :
        ∀ τ ∈ Icc (0:ℝ) 1,
          scalarNormalized v a f (a+T*τ)=flow C (f a) τ := by
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.LinearODE.scalarNormalized, OAI.HarmonicCounterexample.LinearODE.flow

62. def OAI.HarmonicCounterexample.LinearODE.clippedPulse line 1649

    Source documentation

    Constant exterior extension of a pulse coefficient. Its boundedness follows from genuine continuity on the compact pulse, rather than global invertibility of an irrelevant scalar comparison.

    def clippedPulse (C : ℝ → E →L[ℝ] E) : ℝ → E →L[ℝ] E :=
    …

63. lemma OAI.HarmonicCounterexample.LinearODE.clippedPulse_eq line 1653
64. lemma OAI.HarmonicCounterexample.LinearODE.clippedPulse_continuous line 1657
65. lemma OAI.HarmonicCounterexample.LinearODE.clippedPulse_bounded line 1662
66. theorem OAI.HarmonicCounterexample.LinearODE.actual_normalized_value_endpoint line 1699

    Source documentation

    The actual normalized value transmission, not a surrogate first-order solution, is EXACTLY the clipped slow-time operator PB endpoint.

    theorem actual_normalized_value_endpoint
        {A : ℝ → E →L[ℝ] E} {b v : ℝ → ℝ}
        (hA : Continuous A) (hb : Continuous b) {MA Mb : ℝ}
        (hMA : 0 ≤ MA) (hMb : 0 ≤ Mb)
        (hnA : ∀ t,‖A t‖ ≤ MA) (hnb : ∀ t,|b t| ≤ Mb)
        (hpos : ∀ t w,0 ≤ inner ℝ w (A t w)) {l a T : ℝ}
        (hl : 0 < l) (ha : 0 ≤ a) (hT : 0 ≤ T)
        (hvc : ∀ t ∈ Icc a (a+T),ContinuousAt v t) (hvm : StronglyMeasurable v) :
        Real.exp (-(∫ t in a..a+T,v t)) •
          (operatorValue A b l (a+T)*Ring.inverse (operatorValue A b l a)) =
          flow (fun u => ContinuousLinearMap.mul ℝ (E →L[ℝ] E)
            (T • (slope A b l (a+T*clip01 u)-
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.LinearODE.operatorValue, OAI.HarmonicCounterexample.LinearODE.flow, OAI.HarmonicCounterexample.LinearODE.slope, OAI.HarmonicCounterexample.LinearODE.clip01

67. theorem OAI.HarmonicCounterexample.LinearODE.actual_value_inverse_norm_le_one line 1785

    Source documentation

    Positivity produces a contraction bound for the inverse actual value operator. This is uniform over all positive histories and all t >= 0.

    theorem actual_value_inverse_norm_le_one
        {A : ℝ → E →L[ℝ] E} {b : ℝ → ℝ}
        (hA : Continuous A) (hb : Continuous b) {MA Mb : ℝ}
        (hMA : 0 ≤ MA) (hMb : 0 ≤ Mb)
        (hnA : ∀ t,‖A t‖ ≤ MA) (hnb : ∀ t,|b t| ≤ Mb)
        (hpos : ∀ t w,0 ≤ inner ℝ w (A t w)) {l t : ℝ}
        (hl : 0 < l) (ht : 0 ≤ t) :
        ‖Ring.inverse (operatorValue A b l t)‖ ≤ 1 := by
    …

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

68. lemma OAI.HarmonicCounterexample.LinearODE.flowD_norm_bound_pointwise line 1855

    Source documentation

    A coarse finite-time bound used ONLY to justify local parameter differentiation; it is not the uniform-history C1 error constant.

    lemma flowD_norm_bound_pointwise
        (A : H → ℝ → E →L[ℝ] E) (A' : H → ℝ → H →L[ℝ] E →L[ℝ] E)
        {p : H} (hA : Continuous (A p)) (hA' : Continuous (A' p))
        {M : ℝ} (hM : 0 ≤ M) (hb : ∀ s,‖A p s‖ ≤ M) (hb' : ∀ s,‖A' p s‖ ≤ M)
        (x : E) (t : ℝ) : ‖flowD A A' x p t‖ ≤ ‖x‖*Real.exp (2*M*|t|) := by
    …

    Mentions: OAI.HarmonicCounterexample.LinearODE.flowD

69. theorem OAI.HarmonicCounterexample.LinearODE.actual_slope_jet_uniform_bound_on line 1901

    Source documentation

    The finite-time norm bound needed for differentiation under the PB series is PRODUCED for the actual slope and actual full parameter jet, uniformly on the admissible parameter set. No unknown-solution bounds are assumptions.

    theorem actual_slope_jet_uniform_bound_on
        (A : H → ℝ → E →L[ℝ] E) (b : ℝ → ℝ)
        (B' : H → ℝ → H →L[ℝ] OperatorPhase E →L[ℝ] OperatorPhase E)
        (S : Set H) (hA : ∀ p ∈ S,Continuous (A p)) (hb : Continuous b)
        (hB' : ∀ p ∈ S,Continuous (B' p))
        {M MA Mb : ℝ} (hM : 0 ≤ M) (hMA : 0 ≤ MA) (hMb : 0 ≤ Mb)
        (hnB : ∀ p ∈ S,∀ t,‖block (leftAction (A p)) b t‖ ≤ M)
        (hnB' : ∀ p ∈ S,∀ t,‖B' p t‖ ≤ M)
        (hnA : ∀ p ∈ S,∀ t,‖A p t‖ ≤ MA) (hnb : ∀ t,|b t| ≤ Mb)
        (hpos : ∀ p ∈ S,∀ t w,0 ≤ inner ℝ w (A p t w)) {l R : ℝ}
        (hl : 0 < l) : ∃ N : ℝ,0 ≤ N ∧ ∀ p ∈ S,∀ t ∈ Icc 0 R,
          ‖slope (A p) b l t‖ ≤ N ∧ ‖slopeJet A b B' l p t‖ ≤ N := by
    …

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

70. theorem OAI.HarmonicCounterexample.LinearODE.actual_normalized_endpoint_C1 line 2000

    Source documentation

    Actual regular second-order transmission has the uniform C1 endpoint estimate. Its full parameter derivative is genuine. The comparison constant is selected before all histories; finite-time slope/jet bounds needed only for justified differentiation are produced internally from positivity.

    theorem actual_normalized_endpoint_C1
        (e : OrthonormalBasis ι ℝ E) (h : OrthonormalBasis κ ℝ H)
        {C : ℝ} (hC : 0 ≤ C) :
        ∃ J : ℝ,C ≤ J ∧ 0 ≤ J ∧
        ∀ (A : H → ℝ → E →L[ℝ] E) (b v : ℝ → ℝ)
          (K : H → ℝ → H →L[ℝ] OperatorPhase E →L[ℝ] OperatorPhase E)
          (A' : H → ℝ → H →L[ℝ] E →L[ℝ] E)
          (B : H → ℝ → E →L[ℝ] E) (B' : H → ℝ → H →L[ℝ] E →L[ℝ] E)
          (S : Set H) (p : H) (M MA Mb M₀ l a T η : ℝ),
          IsOpen S → IsPreconnected S → p ∈ S →
          (∀ q ∈ S,Continuous (A q)) → Continuous b → Continuous v →
          (∀ q ∈ S,Continuous (K q)) →
    …

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

71. theorem OAI.HarmonicCounterexample.LinearODE.actual_physical_endpoint_C1 line 2136

    Source documentation

    Physical-time Frobenius L1 VALUE and basis-ray JET errors imply the uniform C1 estimate for the ACTUAL second-order transmission. The complete scalar baseline is removed; no pulse-duration factor is introduced.

    theorem actual_physical_endpoint_C1
        (e : OrthonormalBasis ι ℝ E) (h : OrthonormalBasis κ ℝ H)
        {C : ℝ} (hC : 0 ≤ C) :
        ∃ J : ℝ,C ≤ J ∧ 0 ≤ J ∧
        ∀ (A : H → ℝ → E →L[ℝ] E) (b v : ℝ → ℝ)
          (K : H → ℝ → H →L[ℝ] OperatorPhase E →L[ℝ] OperatorPhase E)
          (A' : H → ℝ → H →L[ℝ] E →L[ℝ] E)
          (B : H → ℝ → E →L[ℝ] E) (B' : H → ℝ → H →L[ℝ] E →L[ℝ] E)
          (S : Set H) (p : H) (M MA Mb M₀ l a T η : ℝ),
          IsOpen S → IsPreconnected S → p ∈ S →
          (∀ q ∈ S,Continuous (A q)) → Continuous b → Continuous v →
          (∀ q ∈ S,Continuous (K q)) →
    …

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