OAI/Geometry/HarmonicGrowth/SmoothWord.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicCounterexample.FiniteControl.SmoothWord.step line 16
  2. def OAI.HarmonicCounterexample.FiniteControl.SmoothWord.bump line 17
  3. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.step_smooth line 19
  4. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.step_deriv line 22
  5. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.bump_smooth line 25
  6. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.step_zero line 28
  7. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.step_one line 31
  8. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.bump_zero_after line 34
  9. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.bump_zero_before line 40
  10. def OAI.HarmonicCounterexample.FiniteControl.SmoothWord.state line 48
  11. def OAI.HarmonicCounterexample.FiniteControl.SmoothWord.coefficient line 52
  12. def OAI.HarmonicCounterexample.FiniteControl.SmoothWord.leftWord line 55
  13. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.coefficient_succ line 60
  14. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.coefficient_after line 65
  15. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.state_deriv line 73
  16. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.state_initial line 94
  17. theorem OAI.HarmonicCounterexample.FiniteControl.SmoothWord.state_endpoint line 104

    Source documentation

    Exact ordered exponentials of actual smooth disjoint pulses. This is not an approximation by piecewise-constant coefficient controls.

    theorem state_endpoint (X : ℕ → A) (n : ℕ) {t : ℝ} (ht : 2*(n:ℝ) ≤ t) :
    state X n t=leftWord X n := by
…

    Mentions: OAI.HarmonicCounterexample.FiniteControl.SmoothWord.state, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.leftWord

  18. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.coefficient_smooth line 113
  19. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.coefficient_before line 120
  20. def OAI.HarmonicCounterexample.FiniteControl.SmoothWord.duration line 128

    Source documentation

    Unit-interval pulses have genuine open round gaps at both endpoints.

    def duration (n : ℕ) : ℝ := 2*(n:ℝ)+1
  21. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.duration_pos line 130
  22. def OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitState line 132
  23. def OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitCoefficient line 133
  24. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitState_deriv line 136
  25. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitCoefficient_smooth line 143
  26. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitState_initial line 150
  27. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitState_endpoint line 154
  28. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitCoefficient_zero_outside line 160
  29. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitCoefficient_bounded line 169
  30. def OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitOperator line 195
  31. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitOperator_continuous line 199
  32. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitOperator_bounded line 204
  33. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.actual_flow_eq_state line 211

    Source documentation

    The genuine globally convergent Peano--Baker sum for a smooth disjoint pulse is exactly the explicit ordered-exponential state, not a formal symbol.

    lemma actual_flow_eq_state (X : ℕ → A) (n : ℕ) :
    LinearODE.flow (unitOperator X n) 1 = unitState X n := by
…

    Mentions: OAI.HarmonicCounterexample.LinearODE.flow, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitOperator, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitState

  34. theorem OAI.HarmonicCounterexample.FiniteControl.SmoothWord.actual_flow_endpoint line 221

    Source documentation

    Exact endpoint realization, including the empty word, by actual smooth compactly supported coefficients, with the true initial value 1.

    theorem actual_flow_endpoint (X : ℕ → A) (n : ℕ) :
    LinearODE.flow (unitOperator X n) 1 1=leftWord X n := by
…

    Mentions: OAI.HarmonicCounterexample.LinearODE.flow, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitOperator, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.leftWord

  35. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.bump_deriv_zero_before line 242
  36. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.bump_deriv_zero_after line 249
  37. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packet_intervals_disjoint line 256
  38. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packet_zero_off_interval line 266
  39. theorem OAI.HarmonicCounterexample.FiniteControl.SmoothWord.exists_packet_selector line 276

    Source documentation

    The selector is independent of every word amplitude and parameter. It may jump only outside the active pulse support; no derivative of it is taken.

    theorem exists_packet_selector (n : ℕ) [NeZero n] :
    ∃ d : ℝ → Fin n,∀ t i,i ≠ d t → bump i t=0 ∧ deriv (bump i) t=0 := by
…

    Mentions: OAI.HarmonicCounterexample.FiniteControl.SmoothWord.bump

  40. def OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetScalar line 292
  41. def OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetScalarD line 294
  42. def OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetCoefficient line 296
  43. def OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetCoefficientD line 299
  44. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetCoefficient_deriv line 302
  45. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetCoefficient_smooth line 308
  46. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetCoefficient_selected line 314
  47. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetCoefficient_zero line 335
  48. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetCoefficient_end line 342
  49. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.wide_packet_intervals_disjoint line 367
  50. theorem OAI.HarmonicCounterexample.FiniteControl.SmoothWord.exists_round_gap_selector line 381

    Source documentation

    An angular selector whose jumps lie INSIDE open round gaps. This is stronger than merely vanishing to infinite order at a packet endpoint and matches the metric builder's exact local-constancy-or-round hypothesis.

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

    Mentions: OAI.HarmonicCounterexample.FiniteControl.SmoothWord.bump

  51. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetCoefficient_hasFDerivAt line 442
  52. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetCoefficient_jet_apply line 450
  53. def OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketCoefficient line 455
  54. def OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketCoefficientD line 458
  55. def OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketScalar line 461
  56. def OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketScalarD line 464
  57. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketCoefficient_deriv line 467
  58. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetCoefficientD_smooth line 475
  59. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketCoefficient_smooth line 481
  60. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketCoefficientD_smooth line 485
  61. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketCoefficient_selected line 489
  62. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketCoefficient_zero line 498
  63. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketCoefficient_end line 502
  64. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketCoefficient_hasFDerivAt line 506
  65. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketCoefficient_jet_apply line 512
  66. def OAI.HarmonicCounterexample.FiniteControl.SmoothWord.extendWord line 535
  67. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packetCoefficient_eq_coefficient line 539
  68. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketCoefficient_eq_unitCoefficient line 549
  69. theorem OAI.HarmonicCounterexample.FiniteControl.SmoothWord.actual_packet_endpoint line 555

    Source documentation

    The finite amplitude family used by the switched Berger estimates is exactly the smooth word family, including its order, not merely asymptotic.

    theorem actual_packet_endpoint (a : Fin n → ℝ) (X : Fin n → A) :
    LinearODE.flow (fun t => ContinuousLinearMap.mul ℝ A (unitPacketCoefficient a X t)) 1 1=
      leftWord (extendWord a X) n := by
…

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.LinearODE.flow, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketCoefficient, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.leftWord, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.extendWord

  70. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packet_functions_bounded line 585

    Source documentation

    Fixed global bounds on the actual smooth packets and their time derivatives. These constants do not depend on the word amplitudes.

    lemma packet_functions_bounded (j : ℕ) :
    ∃ C : ℝ,0 ≤ C ∧ ∀ t,|bump j t| ≤ C ∧ |deriv (bump j) t| ≤ C := by
…

    Mentions: OAI.HarmonicCounterexample.FiniteControl.SmoothWord.bump

  71. theorem OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketScalar_uniform_bound line 602

    Source documentation

    Uniform values and time-derivatives on the normalized unit interval (in fact globally). The radius is fixed prior to any choice of amplitudes.

    theorem unitPacketScalar_uniform_bound (n : ℕ) :
    ∃ C : ℝ,0 ≤ C ∧ ∀ (a : Fin n → ℝ) (M : ℝ),
      0 ≤ M → (∀ j,|a j| ≤ M) → ∀ t,
      |unitPacketScalar a t| ≤ C*M ∧ |unitPacketScalarD a t| ≤ C*M := by
…

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketScalar, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketScalarD