OAI/Geometry/HarmonicGrowth/ScalarODE.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicCounterexample.LinearODE.scalar_value_positive line 18

   Source documentation

   Positive scalar initial value cannot cross zero: the equation itself makes y*y' nonnegative and y² nondecreasing.

   lemma scalar_value_positive {A p y v : ℝ → ℝ} (hp : Continuous p)
       (hA : ∀ t,0 ≤ t → 0 ≤ A t)
       (hy : ∀ t,HasDerivAt y (v t) t)
       (hv : ∀ t,HasDerivAt v (A t*y t-p t*v t) t)
       (hy0 : 0 < y 0) (hv0 : 0 ≤ v 0) {t : ℝ} (ht : 0 ≤ t) :
       y 0 ≤ y t ∧ 0 < y t := by
   …

2. def OAI.HarmonicCounterexample.LinearODE.scalarPhase line 52

   Source documentation

   Generic initial data for the actual scalar second-order propagator.

   def scalarPhase (A p : ℝ → ℝ) (a b t : ℝ) : ℝ×ℝ :=
   …

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

3. def OAI.HarmonicCounterexample.LinearODE.scalarU line 55
4. def OAI.HarmonicCounterexample.LinearODE.scalarV line 56
5. lemma OAI.HarmonicCounterexample.LinearODE.scalarPhase_init line 58
6. lemma OAI.HarmonicCounterexample.LinearODE.scalarPhase_deriv line 61
7. lemma OAI.HarmonicCounterexample.LinearODE.scalarPhase_value_deriv line 74
8. lemma OAI.HarmonicCounterexample.LinearODE.scalarPhase_velocity_deriv line 81
9. lemma OAI.HarmonicCounterexample.LinearODE.scalarPhase_linear line 89
10. theorem OAI.HarmonicCounterexample.LinearODE.actual_scalar_leg_nonnegative line 109

    Source documentation

    Positivity is proved for the actual propagation columns, not imposed as an assumption. The estimate is independent of the length of the leg.

    theorem actual_scalar_leg_nonnegative {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)
        (hAp : ∀ t,0 ≤ t → 0 ≤ A t) {t : ℝ} (ht : 0 ≤ t) :
        1 ≤ scalarU A p t ∧ 0 ≤ scalarV A p t := by
    …

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

11. theorem OAI.HarmonicCounterexample.LinearODE.actual_scalar_normalizer_bounds line 139

    Source documentation

    The uniform K bound in manuscript (full-normalization), with U and V produced by the actual scalar ODE.

    theorem actual_scalar_normalizer_bounds {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)
        (hAp : ∀ t,0 ≤ t → 0 ≤ A t) {t θ : ℝ} (ht : 0 ≤ t) (hθ : 0 < θ) :
        0 < scalarU A p t+θ*scalarV A p t ∧
          0 ≤ scalarV A p t/(scalarU A p t+θ*scalarV A p t) ∧
          scalarV A p t/(scalarU A p t+θ*scalarV A p t) ≤ θ⁻¹ := by
    …

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

12. lemma OAI.HarmonicCounterexample.LinearODE.scalar_velocity_positive line 171
13. theorem OAI.HarmonicCounterexample.LinearODE.actual_scalar_leg_positive line 196

    Source documentation

    Both diagonal propagation columns are genuinely STRICTLY positive at positive leg times, as claimed in the manuscript.

    theorem actual_scalar_leg_positive {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)
        (hAp : ∀ t,0 ≤ t → 0 ≤ A t) {t : ℝ} (ht : 0 < t) :
        0 < scalarU A p t ∧ 0 < scalarV A p t := by
    …

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

14. def OAI.HarmonicCounterexample.LinearODE.scalarBaseline line 234

    Source documentation

    The exact parameter-free scalar baseline, produced from the convergent Peano--Baker solution rather than assumed as a Riccati solution.

    def scalarBaseline (A p : ℝ → ℝ) (θ t : ℝ) : ℝ :=
    …

15. lemma OAI.HarmonicCounterexample.LinearODE.scalarBaseline_init line 237
16. lemma OAI.HarmonicCounterexample.LinearODE.actual_scalar_baseline_positive line 240
17. lemma OAI.HarmonicCounterexample.LinearODE.actual_scalar_baseline_deriv line 260
18. theorem OAI.HarmonicCounterexample.LinearODE.actual_scalar_baseline_close line 278

    Source documentation

    The exact baseline remains uniformly close to the limiting positive root. The estimate has no pulse-duration factor, and is independent of all current control parameters and of incoming matrix Riccati data.

    theorem actual_scalar_baseline_close {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)
        (hAp : ∀ t,0 ≤ t → 0 ≤ A t) {θ γ M T : ℝ}
        (hθ : 0 ≤ θ) (hγ : 0 < γ) (hM : 0 ≤ M)
        (hpl : ∀ t ∈ Set.Icc 0 T,γ ≤ p t)
        (hF : ∀ t ∈ Set.Icc 0 T,|A t-p t*θ-θ^2| ≤ M) :
        ∀ t ∈ Set.Icc 0 T,|scalarBaseline A p θ t-θ| ≤ M/γ := by
    …

    Mentions: OAI.HarmonicCounterexample.LinearODE.scalarBaseline