PulseODE.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HarmonicCounterexample.LinearODE.slow_residual_identity line 20

Source documentation

Exact scalar-baseline cancellation. Keeping v exact removes a term of size (a-a_*) times the long pulse duration.

lemma slow_residual_identity (A₀ p p₀ v θ τ : ℝ) (S Sdot Err : R) :
    (A₀ • (1:R)+((p₀+2*θ)*τ) • S+Err)-
      p • (v • (1:R)+τ • S)-(v • (1:R)+τ • S)*(v • (1:R)+τ • S)-
      ((A₀-p*v-v^2) • (1:R)+(τ^2) • Sdot) =
      Err+((p₀+2*θ-p-2*v)*τ) • S-(τ^2) • (S*S+Sdot) := by
…

lemma OAI.HarmonicCounterexample.LinearODE.slow_residual_jet_identity line 30

Source documentation

Exact first parameter derivative of that residual. The scalar baseline and p are independent of the CURRENT control parameter.

lemma slow_residual_jet_identity (p p₀ v θ τ : ℝ) (S Sh Shdot Errh : R) :
    (((p₀+2*θ)*τ) • Sh+Errh)-p • (τ • Sh)-
      (τ • Sh)*(v • (1:R)+τ • S)-(v • (1:R)+τ • S)*(τ • Sh)-
      (τ^2) • Shdot =
      Errh+((p₀+2*θ-p-2*v)*τ) • Sh-(τ^2) • (Sh*S+S*Sh+Shdot) := by
…

lemma OAI.HarmonicCounterexample.LinearODE.slow_residual_bound line 39

Source documentation

A uniform slow-pulse residual bound with completely explicit constants.

lemma slow_residual_bound {Err S Sdot : R} {C δ τ ε : ℝ}
    (hC : 0 ≤ C) (hδ : 0 ≤ δ) (hτ : 0 ≤ τ)
    (he : ‖Err‖ ≤ C*(δ*τ+τ^2)) (hε : |ε| ≤ 3*C*δ)
    (hS : ‖S‖ ≤ C) (hSd : ‖Sdot‖ ≤ C) :
    ‖Err+(ε*τ) • S-(τ^2) • (S*S+Sdot)‖ ≤
      (3*C^2+2*C)*(δ*τ+τ^2) := by
…

lemma OAI.HarmonicCounterexample.LinearODE.slow_residual_jet_bound line 60
def OAI.HarmonicCounterexample.LinearODE.bergerSlowGenerator line 100
Source documentation
The source's first-order slow generator, including its precise Riccati denominator. The angular infinitesimal is r B Id+D.
```
def bergerSlowGenerator (r B β p₀ θ z : ℝ) (D : R) : R :=
…
```

theorem OAI.HarmonicCounterexample.LinearODE.berger_comparison_residuals line 107

Source documentation

Uniform residual AND true parameter-direction residual estimates for the exact Berger comparison. The constant is chosen before the scalar history, small deviation, duration, pulse position and parameters. All nonlinear angular remainders are proved, not hypotheses.

theorem berger_comparison_residuals (r B β p₀ θ : ℝ) (D : R)
    {M Z K : ℝ} (hM : 0 ≤ M) (hZ : 0 ≤ Z) (hK : 0 ≤ K)
    (hc : p₀+2*θ ≠ 0) :
    ∃ C : ℝ,0 ≤ C ∧ ∀ α p v δ τ z zd zh zhd : ℝ,
      0 ≤ δ → 0 ≤ τ → |α| ≤ M → |α-β| ≤ δ → |p-p₀| ≤ δ → |v-θ| ≤ K*δ →
      |z| ≤ Z → |zd| ≤ Z → |zh| ≤ Z → |zhd| ≤ Z →
      1+τ*z ∈ Set.Icc (1/2:ℝ) (3/2) →
      let S := bergerSlowGenerator r B β p₀ θ z D
…

Mentions: OAI.HarmonicCounterexample.LinearODE.bergerSlowGenerator

theorem OAI.HarmonicCounterexample.LinearODE.berger_scalar_baseline_close line 197

Source documentation

The exact source scalar baseline, forced by B/a(t)^2, deviates from its limiting root by O(delta), uniformly in the pulse length.

theorem berger_scalar_baseline_close {α p : ℝ → ℝ}
    (hα : Continuous α) (hp : Continuous p)
    {M Mp B β p₀ θ γ δ T : ℝ}
    (hM : 0 ≤ M) (hMp : 0 ≤ Mp) (hθ : 0 ≤ θ) (hγ : 0 < γ) (hδ : 0 ≤ δ)
    (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 ∈ Icc 0 T,|scalarBaseline (fun s => α s*B) p θ t-θ| ≤
      ((|B|+|θ|)/γ)*δ := by
…

Mentions: OAI.HarmonicCounterexample.LinearODE.scalarBaseline

theorem OAI.HarmonicCounterexample.LinearODE.actual_berger_comparison_residuals line 231

Source documentation

Model-specific residuals with the actual scalar PB baseline substituted. The resulting C is fixed BEFORE all histories, scalar coefficient functions, period lengths, pulse positions and control parameters. This is the analytic uniformity required for recursive attainment, not a compactness claim about an unspecified incoming Riccati matrix.

theorem actual_berger_comparison_residuals (r B β p₀ θ γ : ℝ) (D : R)
    {M Z : ℝ} (hM : 0 ≤ M) (hZ : 0 ≤ Z) (hθ : 0 ≤ θ) (hγ : 0 < γ)
    (hc : p₀+2*θ ≠ 0) (hroot : β*B-p₀*θ-θ^2=0) :
    ∃ C : ℝ,0 ≤ C ∧ ∀ (α p : ℝ → ℝ) (Mp δ T τ : ℝ),
      Continuous α → Continuous p → 0 ≤ Mp → 0 ≤ δ → 0 ≤ τ →
      (∀ t,|α t| ≤ M) → (∀ t,|p t| ≤ Mp) →
      (∀ t,0 ≤ t → 0 ≤ α t*B) →
      (∀ t ∈ Icc 0 T,|α t-β| ≤ δ) →
      (∀ t ∈ Icc 0 T,|p t-p₀| ≤ δ) →
      (∀ t ∈ Icc 0 T,γ ≤ p t) →
      ∀ t ∈ Icc 0 T,∀ z zd zh zhd : ℝ,
        |z| ≤ Z → |zd| ≤ Z → |zh| ≤ Z → |zhd| ≤ Z →
…

lemma OAI.HarmonicCounterexample.LinearODE.bergerComparison_time_deriv line 281

Source documentation

The tau-square factor in the source residual is the TRUE time derivative of the rescaled comparison, not a syntactically assigned jet.

lemma bergerComparison_time_deriv (r B β p₀ θ τ : ℝ) (D : R)
    {v z : ℝ → ℝ} {v' z' t : ℝ}
    (hv : HasDerivAt v v' t) (hz : HasDerivAt z z' (τ*t)) :
    HasDerivAt (fun s => v s • (1:R)+τ • bergerSlowGenerator r B β p₀ θ (z (τ*s)) D)
      (v' • (1:R)+(τ^2) • bergerSlowGenerator r B β p₀ θ z' D) t := by
…

Mentions: OAI.HarmonicCounterexample.LinearODE.bergerSlowGenerator

lemma OAI.HarmonicCounterexample.LinearODE.bergerComparison_parameter_deriv line 297

Source documentation

The comparison's parameter variation is its GENUINE Frechet derivative; the exact scalar baseline is independent of the current control parameter.

lemma bergerComparison_parameter_deriv (r B β p₀ θ τ v : ℝ) (D : R)
    {z : H → ℝ} {z' : H →L[ℝ] ℝ} {x : H} (hz : HasFDerivAt z z' x) :
    HasFDerivAt (fun y => v • (1:R)+τ • bergerSlowGenerator r B β p₀ θ (z y) D)
      (z'.smulRight (τ • bergerSlowGenerator r B β p₀ θ 1 D)) x := by
…

Mentions: OAI.HarmonicCounterexample.LinearODE.bergerSlowGenerator

lemma OAI.HarmonicCounterexample.LinearODE.bergerAngular_parameter_deriv line 311

Source documentation

True directional derivative of the exact Berger angular coefficient, including the current scale alpha and slow-pulse factor tau.

lemma bergerAngular_parameter_deriv (r B α τ : ℝ) (D : R)
    {z : H → ℝ} {z' : H →L[ℝ] ℝ} {x : H} (hz : HasFDerivAt z z' x)
    (hq : 1+τ*z x ≠ 0) :
    HasFDerivAt (fun y => α • PulseTaylor.angular r (B • (1:R)) D (1+τ*z y))
      (z'.smulRight ((α*τ) • PulseTaylor.angularD r (B • (1:R)) D (1+τ*z x))) x := by
…

Mentions: OAI.HarmonicCounterexample.PulseTaylor.angular, OAI.HarmonicCounterexample.PulseTaylor.angularD

lemma OAI.HarmonicCounterexample.LinearODE.scalar_plus_small_positive line 344
Source documentation
Positivity of the comparison follows from a small pulse and the actual positive scalar baseline. Symmetry is not used or silently assumed here.
```
lemma scalar_plus_small_positive {S : E →L[ℝ] E} {v τ C : ℝ}
    (hτ : 0 ≤ τ) (hSn : ‖S‖ ≤ C) (hgap : τ*C ≤ v) :
    ∀ x : E,0 ≤ inner ℝ x ((v • (1:E →L[ℝ] E)+τ • S) x) := by
…
```
lemma OAI.HarmonicCounterexample.LinearODE.scalarBaseline_stronglyMeasurable line 377
Source documentation
Global measurability of the genuine quotient holds even at irrelevant negative-time zeros. No global nonvanishing hypothesis is needed for FTC.
```
lemma scalarBaseline_stronglyMeasurable {A 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) (θ : ℝ) :
    StronglyMeasurable (scalarBaseline A p θ) := by
…
```
Mentions: OAI.HarmonicCounterexample.LinearODE.scalarBaseline
def OAI.HarmonicCounterexample.LinearODE.actualBergerComparison line 394
Source documentation
The actual comparison used in the slow pulse: the scalar part is built from PB flow, not chosen as an unproved solution of a Riccati equation.
```
def actualBergerComparison (α p : ℝ → ℝ) (r B β p₀ θ τ : ℝ) (D : R)
    (z : ℝ → ℝ) (t : ℝ) : R :=
…
```
lemma OAI.HarmonicCounterexample.LinearODE.actualBergerComparison_deriv line 399
lemma OAI.HarmonicCounterexample.LinearODE.actualBergerComparison_initial line 412

lemma OAI.HarmonicCounterexample.LinearODE.actualBergerComparison_parameter_deriv line 422

Source documentation

The comparison's parameter jet is actual Frechet differentiation of the PB-based expression. The baseline does not depend on the current parameter.

lemma actualBergerComparison_parameter_deriv (α p : ℝ → ℝ) (r B β p₀ θ τ : ℝ) (D : R)
    {z : H → ℝ → ℝ} {z' : H →L[ℝ] ℝ} {x : H} (t : ℝ)
    (hz : HasFDerivAt (fun y => z y (τ*t)) z' x) :
    HasFDerivAt (fun y => actualBergerComparison α p r B β p₀ θ τ D (z y) t)
      (z'.smulRight (τ • bergerSlowGenerator r B β p₀ θ 1 D)) x :=
…

Mentions: OAI.HarmonicCounterexample.LinearODE.actualBergerComparison, OAI.HarmonicCounterexample.LinearODE.bergerSlowGenerator

lemma OAI.HarmonicCounterexample.LinearODE.scalar_plus_small_coercive line 446

lemma OAI.HarmonicCounterexample.LinearODE.actualBergerComparison_coercive line 462

Source documentation

Uniform positivity of the actual comparison is derived from the actual baseline estimate and smallness conditions, not assumed for the Riccati bound.

lemma actualBergerComparison_coercive {α p : ℝ → ℝ}
    (hα : Continuous α) (hp : Continuous p) {M Mp B β p₀ θ γ δ T τ r Z : ℝ}
    (hM : 0 ≤ M) (hMp : 0 ≤ Mp) (hθ : 0 ≤ θ) (hγ : 0 < γ) (hδ : 0 ≤ δ)
    (hτ : 0 ≤ τ) (hαn : ∀ t,|α t| ≤ M) (hpn : ∀ t,|p t| ≤ Mp)
    (hAp : ∀ t,0 ≤ t → 0 ≤ α t*B) (hroot : β*B-p₀*θ-θ^2=0)
    (hscale : ∀ t ∈ Set.Icc 0 T,|α t-β| ≤ δ)
    (hpt : ∀ t ∈ Set.Icc 0 T,|p t-p₀| ≤ δ)
    (hpl : ∀ t ∈ Set.Icc 0 T,γ ≤ p t)
    (D : E →L[ℝ] E) {z : ℝ → ℝ}
    (hz : ∀ t ∈ Set.Icc 0 T,|z (τ*t)| ≤ Z)
    (hsmall : ((|B|+|θ|)/γ)*δ+
      τ*(|β/(p₀+2*θ)| * Z * ‖r • (B • (1:E →L[ℝ] E))+D‖) ≤ θ/2) :
…

theorem OAI.HarmonicCounterexample.LinearODE.actual_berger_pulse_integrated line 523

Source documentation

Actual Berger pulse, with the nonlinear angular coefficient and exact scalar Peano--Baker baseline substituted into the actual center-regular Riccati and variational equations. The constant is chosen before all histories, start times, durations, scalar backgrounds, and pulse shapes.

theorem actual_berger_pulse_integrated (basis : OrthonormalBasis ι ℝ E)
    (r B β p₀ θ γ : ℝ) (D : E →L[ℝ] E) {M Z : ℝ}
    (hM : 0 ≤ M) (hZ : 0 ≤ Z) (hθ : 0 ≤ θ) (hγ : 0 < γ)
    (hc : p₀+2*θ ≠ 0) (hroot : β*B-p₀*θ-θ^2=0) :
    ∃ C : ℝ,1 ≤ C ∧ ∀ (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 z zd zh zhd : ℝ → ℝ) (Mp MB MA Mb l B₀ a T δ ε : ℝ),
      Continuous (A x) → Continuous b → Continuous (B' x) →
      Continuous (fun t => A' x t h) →
      (∀ t v w,B' x t v w=(0,A' x t v*w.1)) →
      0 ≤ MB → 0 ≤ MA → 0 ≤ Mb →
…

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

theorem OAI.HarmonicCounterexample.LinearODE.actual_switched_berger_estimates line 736

Source documentation

Actual finite switched Berger word: its angular generator can change on round gaps. The smooth first-order coefficient and its derivative are supplied by the explicit finite pulse family, not by differentiating a discontinuous selector. Nonlinear residuals are produced uniformly over the FINITE library. The one constant is chosen before every history, selector, shape and duration.

theorem actual_switched_berger_estimates (basis : OrthonormalBasis ι ℝ E)
    (r B β p₀ θ γ : ℝ) (D : κ → E →L[ℝ] E) {M Z : ℝ}
    (hM : 0 ≤ M) (hZ : 0 ≤ Z) (hθ : 0 ≤ θ) (hγ : 0 < γ)
    (hc : p₀+2*θ ≠ 0) (hroot : β*B-p₀*θ-θ^2=0) :
    ∃ C : ℝ,1 ≤ C ∧ ∀ (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 z zd zh zhd : ℝ → ℝ) (d : ℝ → κ)
      (S Sd Sh Shd : ℝ → E →L[ℝ] E) (Mp MB MA Mb l B₀ a T δ ε : ℝ),
      Continuous (A x) → Continuous b → Continuous (B' x) →
      Continuous (fun t => A' x t h) →
      (∀ t v w,B' x t v w=(0,A' x t v*w.1)) →
…

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