OAI/Geometry/HarmonicGrowth/InsertedWord.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearPacket line 26

   Source documentation

   Actual nonlinear angular coefficients are glued by their deviations from roundness. This finite sum is smooth without differentiating a discontinuous angular selector. On disjoint packet supports it is exactly the Berger model.

   def nonlinearPacket (r : ℝ) (b : E) (D : ι → E) (q : ι → ℝ) : E :=
   …

   Mentions: OAI.HarmonicCounterexample.b

2. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearPacket_selected line 29
3. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearPacket_smooth line 41

   Source documentation

   Smoothness of the actual finite nonlinear coefficient, including all round gaps. Positivity excludes the sole singularity of real-power calculus.

   lemma nonlinearPacket_smooth (r : ℝ) (b : E) (D : ι → E) (q : ι → H → ℝ)
       (hq : ∀ j,ContDiff ℝ ∞ (q j)) (hne : ∀ j x,q j x ≠ 0) :
       ContDiff ℝ ∞ (fun x => nonlinearPacket r b D (fun j => q j x)) := by
   …

   Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearPacket

4. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearPacket_hasFDerivAt line 53

   Source documentation

   The full parameter jet of the true nonlinear family, not a formal linearized coefficient supplied as an assumption.

   lemma nonlinearPacket_hasFDerivAt (r : ℝ) (b : E) (D : ι → E) (q : ι → H → ℝ)
       (q' : ι → H →L[ℝ] ℝ) (x : H) (hq : ∀ j,HasFDerivAt (q j) (q' j) x)
       (hne : ∀ j,q j x ≠ 0) :
       HasFDerivAt (fun y => nonlinearPacket r b D (fun j => q j y))
         (∑ j,(q' j).smulRight (PulseTaylor.angularD r b (D j) (q j x))) x := by
   …

   Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearPacket, OAI.HarmonicCounterexample.PulseTaylor.angularD

5. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearPacket_jet_selected line 65
6. def OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetStretch line 98

   Source documentation

   Stretch inside one of the disjoint unit-time packets.

   def packetStretch (a : Fin n → ℝ) (T t : ℝ) (j : Fin n) : ℝ :=
   …

   Mentions: OAI.HarmonicCounterexample.a

7. def OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearBergerWord line 101
8. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetStretch_selected line 104
9. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearBergerWord_selected line 117

   Source documentation

   Exact actual Berger operator on each pulse, with round interpolation in all gaps. The scalar and angular parts are genuinely the source model.

   lemma nonlinearBergerWord_selected (r : ℝ) (b : E) (D : Fin n → E) (a : Fin n → ℝ)
       (T t : ℝ) (d : Fin n) (hd : ∀ j,j ≠ d → bump j (duration n*t)=0) :
       nonlinearBergerWord r b D a T t=
         PulseTaylor.angular r b (D d) (1+T⁻¹*unitPacketScalar a t) := by
   …

   Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.bump, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.duration, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearBergerWord, OAI.HarmonicCounterexample.PulseTaylor.angular, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketScalar

10. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetStretch_smooth line 127
11. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearBergerWord_smooth line 133
12. theorem OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetStretch_uniform_positive line 162

    Source documentation

    A fixed amplitude bound gives positive stretches for all sufficiently long physical packets. The threshold is chosen before the amplitudes and before any incoming ODE history.

    theorem packetStretch_uniform_positive (n : ℕ) :
        ∃ C : ℝ,0 ≤ C ∧ ∀ (a : Fin n → ℝ) (U T : ℝ),0 ≤ U →
          (∀ j,|a j| ≤ U) → 0 < T → 2*C*U ≤ T → ∀ t j,
          packetStretch a T t j ∈ Icc (1/2:ℝ) (3/2) := by
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetStretch

13. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetStretch_hasFDerivAt line 195
14. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearBergerWord_hasFDerivAt line 205

    Source documentation

    The endpoint family uses the genuine Frechet derivative of the smooth nonlinear angular coefficient, including parameter variation in the packets.

    lemma nonlinearBergerWord_hasFDerivAt (r : ℝ) (b : E) (D : Fin n → E)
        (a : Fin n → H → ℝ) (a' : Fin n → H →L[ℝ] ℝ) {x : H}
        (ha : ∀ j,HasFDerivAt (a j) (a' j) x) (T t : ℝ)
        (hne : ∀ j,packetStretch (fun k => a k x) T t j ≠ 0) :
        HasFDerivAt (fun y => nonlinearBergerWord r b D (fun j => a j y) T t)
          (∑ j : Fin n,((T⁻¹*duration n*bump j (duration n*t)) • a' j).smulRight
            (PulseTaylor.angularD r b (D j) (packetStretch (fun k => a k x) T t j))) x :=
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetStretch, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearBergerWord, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.duration, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.bump, OAI.HarmonicCounterexample.PulseTaylor.angularD

15. theorem OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearBergerWord_smooth_for_long_packets line 219

    Source documentation

    A duration threshold alone suffices for a globally smooth actual Berger word. Nonzero stretches are proved, rather than left as assumptions.

    theorem nonlinearBergerWord_smooth_for_long_packets (n : ℕ) :
        ∃ C : ℝ,0 ≤ C ∧ ∀ (r : ℝ) (b : E) (D : Fin n → E) (a : Fin n → ℝ)
          (U T : ℝ),0 ≤ U → (∀ j,|a j| ≤ U) → 0 < T → 2*C*U ≤ T →
          ContDiff ℝ ∞ (nonlinearBergerWord r b D a T) := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearBergerWord

16. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearPacket_round line 250
17. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearBergerWord_round_before line 254
18. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearBergerWord_round_after line 266
19. theorem OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearBergerWord_round_collars line 280

    Source documentation

    A fixed round collar at each end works for every amplitude vector and every physical duration. This allows smooth rotation of complex structures in the gaps without changing the angular metric.

    theorem nonlinearBergerWord_round_collars (n : ℕ) (r : ℝ) (b : E) (D : Fin n → E) :
        (∀ᶠ t in 𝓝 (0:ℝ),∀ a T,nonlinearBergerWord r b D a T t=b) ∧
        (∀ᶠ t in 𝓝 (1:ℝ),∀ a T,nonlinearBergerWord r b D a T t=b) := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearBergerWord

20. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.berger_angular_nonneg line 319

    Source documentation

    Positivity of the actual Berger angular operator follows from the vertical square spectral interval [-B,0], not from a separate positivity hypothesis on the produced perturbed operator.

    lemma berger_angular_nonneg (r B q : ℝ) (D : E →L[ℝ] E) (hq : 0 ≤ q)
        (hD : ∀ x,inner ℝ x (D x) ≤ 0)
        (hBD : ∀ x,-(B*‖x‖^2) ≤ inner ℝ x (D x)) (x : E) :
        0 ≤ inner ℝ x (PulseTaylor.angular r (B • (1:E →L[ℝ] E)) D q x) := by
    …

    Mentions: OAI.HarmonicCounterexample.PulseTaylor.angular

21. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearBergerWord_nonneg line 339

    Source documentation

    Each actual finite pulse is nonnegative for every vector. Positivity is inherited from exact disjoint-support reduction to the source angular formula, including the round gaps.

    lemma nonlinearBergerWord_nonneg {n : ℕ} (r B : ℝ) (D : Fin n → E →L[ℝ] E)
        (a : Fin n → ℝ) (T t : ℝ) (d : Fin n)
        (hd : ∀ j,j ≠ d → bump j (duration n*t)=0)
        (hq : 0 ≤ packetStretch a T t d)
        (hD : ∀ j x,inner ℝ x (D j x) ≤ 0)
        (hBD : ∀ j x,-(B*‖x‖^2) ≤ inner ℝ x (D j x)) (x : E) :
        0 ≤ inner ℝ x (nonlinearBergerWord r (B • (1:E →L[ℝ] E)) D a T t x) := by
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.bump, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.duration, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetStretch, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearBergerWord

22. def OAI.HarmonicCounterexample.FiniteControl.SmoothWord.insertWord line 374

    Source documentation

    Replace only the angular part of an incoming coefficient history on one new pulse. The formula is global and smooth, with no piecewise selector.

    def insertWord (history : ℝ → E) (α : ℝ → ℝ) (r : ℝ) (b : E)
        (D : Fin n → E) (amps : Fin n → ℝ) (a T t : ℝ) : E :=
    …

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

23. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.insertWord_before line 378
24. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.insertWord_after line 386
25. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.insertWord_on_round line 396
26. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.insertWord_smooth line 404
27. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.insertWord_jet_history_zero line 414

    Source documentation

    The actual parameter jet is exactly zero throughout the preceding history, for arbitrary parameter dependence of the new amplitudes.

    lemma insertWord_jet_history_zero (history : ℝ → E) (α : ℝ → ℝ)
        (r : ℝ) (b : E) (D : Fin n → E) (amps : H → Fin n → ℝ)
        (a T t : ℝ) (hT : 0 < T) (ht : t ≤ a) (x : H) :
        fderiv ℝ (fun y => insertWord history α r b D (amps y) a T t) x=0 := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.insertWord

28. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearBergerWord_jet_selected line 446
29. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearBergerWord_fderiv_ray_selected line 475

    Source documentation

    The exact jet hypothesis in the actual finite Berger error theorem is supplied by differentiation of the actual smooth coefficient family.

    lemma nonlinearBergerWord_fderiv_ray_selected (r : ℝ) (b : E) (D : Fin n → E)
        (a : Fin n → H → ℝ) (a' : Fin n → H →L[ℝ] ℝ) {x : H}
        (ha : ∀ j,HasFDerivAt (a j) (a' j) x) (T t : ℝ)
        (hne : ∀ j,packetStretch (fun k => a k x) T t j ≠ 0)
        (d : Fin n) (hd : ∀ j,j ≠ d → bump j (duration n*t)=0) (v : H) :
        fderiv ℝ (fun y => nonlinearBergerWord r b D (fun j => a j y) T t) x v=
          (T⁻¹*unitPacketScalar (fun j => a' j v) t) •
            PulseTaylor.angularD r b (D d) (1+T⁻¹*unitPacketScalar (fun j => a j x) t) := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetStretch, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.bump, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.duration, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearBergerWord, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketScalar, OAI.HarmonicCounterexample.PulseTaylor.angularD

30. theorem OAI.HarmonicCounterexample.FiniteControl.SmoothWord.actual_smooth_positive_word line 512

    Source documentation

    A uniform finite angular producer: every sufficiently long packet gives a smooth nonnegative actual coefficient for every permitted amplitude vector. The threshold is independent of the incoming ODE history.

    theorem actual_smooth_positive_word (n : ℕ) [NeZero n] :
        ∃ C : ℝ,0 ≤ C ∧ ∀ (r B : ℝ) (D : Fin n → E →L[ℝ] E)
          (a : Fin n → ℝ) (U T : ℝ),0 ≤ U → (∀ j,|a j| ≤ U) → 0 < T → 2*C*U ≤ T →
          (∀ j x,inner ℝ x (D j x) ≤ 0) →
          (∀ j x,-(B*‖x‖^2) ≤ inner ℝ x (D j x)) →
          ContDiff ℝ ∞ (nonlinearBergerWord r (B • (1:E →L[ℝ] E)) D a T) ∧
          ∀ t x,0 ≤ inner ℝ x (nonlinearBergerWord r (B • (1:E →L[ℝ] E)) D a T t x) := by
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearBergerWord

31. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.insertWord_nonneg line 531
32. lemma OAI.HarmonicCounterexample.LinearODE.operator_history_eq line 578
33. lemma OAI.HarmonicCounterexample.LinearODE.slope_history_eq line 590

    Source documentation

    The actual center-regular Riccati value is causal, even though it is represented by one globally defined Peano--Baker sum.

    lemma slope_history_eq {A B : ℝ → E →L[ℝ] E} {T : ℝ}
        (h : EqOn A B (Icc 0 T)) (p : ℝ → ℝ) (l : ℝ) {t : ℝ} (ht : t ∈ Icc 0 T) :
        slope A p l t=slope B p l t := by
    …

    Mentions: OAI.HarmonicCounterexample.LinearODE.slope

34. lemma OAI.HarmonicCounterexample.LinearODE.slopeJet_history_zero line 596
35. lemma OAI.HarmonicCounterexample.LinearODE.insertWord_incoming_slope line 605

    Source documentation

    The new control never perturbs its incoming center-regular slope.

    lemma insertWord_incoming_slope {n : ℕ} (history : ℝ → E →L[ℝ] E) (α : ℝ → ℝ)
        (r : ℝ) (b : E →L[ℝ] E) (D : Fin n → E →L[ℝ] E)
        (amps : Fin n → ℝ) (a T : ℝ) (hT : 0 < T) (ha : 0 ≤ a)
        (p : ℝ → ℝ) (l : ℝ) :
        slope (FiniteControl.SmoothWord.insertWord history α r b D amps a T) p l a=
          slope history p l a := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.LinearODE.slope, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.insertWord

36. lemma OAI.HarmonicCounterexample.LinearODE.insertWord_incoming_slopeJet line 617

    Source documentation

    The actual incoming parameter jet vanishes, not merely an arbitrarily assigned initial derivative for a restarted surrogate equation.

    lemma insertWord_incoming_slopeJet {n : ℕ} (history : ℝ → E →L[ℝ] E) (α : ℝ → ℝ)
        (r : ℝ) (b : E →L[ℝ] E) (D : Fin n → E →L[ℝ] E)
        (amps : H → Fin n → ℝ) (a T : ℝ) (hT : 0 < T) (ha : 0 ≤ a)
        (p : ℝ → ℝ) (l : ℝ) (x : H) :
        let A := fun y => FiniteControl.SmoothWord.insertWord history α r b D (amps y) a T
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.insertWord

37. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.insertWord_hasFDerivAt line 659

    Source documentation

    The history insertion has the genuine full parameter derivative of the nonlinear Berger coefficient; the preceding history is not differentiated.

    lemma insertWord_hasFDerivAt (history : ℝ → E) (α : ℝ → ℝ)
        (r : ℝ) (b : E) (D : Fin n → E) (amps : Fin n → H → ℝ)
        (amps' : Fin n → H →L[ℝ] ℝ) {x : H}
        (ha : ∀ j,HasFDerivAt (amps j) (amps' j) x) (a T t : ℝ)
        (hne : ∀ j,packetStretch (fun k => amps k x) T ((t-a)/T) j ≠ 0) :
        HasFDerivAt (fun y => insertWord history α r b D (fun j => amps j y) a T t)
          (α t • ∑ j : Fin n,
            ((T⁻¹*duration n*bump j (duration n*((t-a)/T))) • amps' j).smulRight
              (PulseTaylor.angularD r b (D j)
                (packetStretch (fun k => amps k x) T ((t-a)/T) j))) x := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetStretch, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.insertWord, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.duration, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.bump, OAI.HarmonicCounterexample.PulseTaylor.angularD

38. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.insertWord_fderiv_ray_selected line 671
39. lemma OAI.HarmonicCounterexample.LinearODE.block_parameter_jet_exists line 708
40. lemma OAI.HarmonicCounterexample.LinearODE.operator_block_parameter_jet_exists line 756

    Source documentation

    The precise phase derivative required by the actual endpoint estimates is produced from differentiation of the angular coefficient.

    lemma operator_block_parameter_jet_exists {A : H → ℝ → E →L[ℝ] E}
        {A' : H →L[ℝ] E →L[ℝ] E} {x : H} (b : ℝ → ℝ) (t : ℝ)
        (hA : HasFDerivAt (fun q => A q t) A' x) :
        ∃ K : H →L[ℝ] (((E →L[ℝ] E)×(E →L[ℝ] E)) →L[ℝ]
           ((E →L[ℝ] E)×(E →L[ℝ] E))),
          HasFDerivAt (fun q => block (leftAction (A q)) b t) K x ∧
          ∀ h w,K h w=(0,A' h*w.1) := by
    …

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

41. lemma OAI.HarmonicCounterexample.PulseTaylor.angularD_comp_smooth line 789
42. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearBergerWord_jet_smooth line 819

    Source documentation

    The actual full coefficient jet is smooth in time, including the round collars where the discrete angular selector changes.

    lemma nonlinearBergerWord_jet_smooth (r : ℝ) (b : E) (D : Fin n → E)
        (amps : Fin n → ℝ) (amps' : Fin n → H →L[ℝ] ℝ) (T : ℝ)
        (hne : ∀ j t,packetStretch amps T t j ≠ 0) :
        ContDiff ℝ ∞ (fun t => ∑ j : Fin n,
          ((T⁻¹*duration n*bump j (duration n*t)) • amps' j).smulRight
            (PulseTaylor.angularD r b (D j) (packetStretch amps T t j))) := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetStretch, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.duration, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.bump, OAI.HarmonicCounterexample.PulseTaylor.angularD

43. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.insertWord_actual_jet_smooth line 831
44. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.insertWord_jet_after_zero line 872
45. theorem OAI.HarmonicCounterexample.FiniteControl.SmoothWord.insertWord_actual_jet_bound line 886

    Source documentation

    A genuine global-in-time bound for the actual parameter jet. The bound is selected before the incoming coefficient history, since that history does not vary with the current control parameters.

    theorem insertWord_actual_jet_bound (α : ℝ → ℝ) (hα : ContDiff ℝ ∞ α)
        (r : ℝ) (b : E) (D : Fin n → E) (amps : Fin n → H → ℝ)
        (amps' : Fin n → H →L[ℝ] ℝ) {x : H}
        (ha : ∀ j,HasFDerivAt (amps j) (amps' j) x) (a T : ℝ) (hT : 0 < T)
        (hne : ∀ j t,packetStretch (fun k => amps k x) T t j ≠ 0) :
        ∃ M : ℝ,0 ≤ M ∧ ∀ (history : ℝ → E) (t : ℝ),
          ‖fderiv ℝ (fun y => insertWord history α r b D (fun j => amps j y) a T t) x‖ ≤ M := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetStretch, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.insertWord