OAI/Geometry/HarmonicGrowth/EndpointBounds.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HarmonicCounterexample.PulseTaylor.angular_uniform_bounds line 14

   Source documentation

   Uniform value and derivative bounds on the fixed positive stretch interval. These are bounds for the actual nonlinear Berger formula.

   theorem angular_uniform_bounds (r : ℝ) (b D : E) :
       ∃ C : ℝ, 0 ≤ C ∧ ∀ q ∈ Icc (1/2:ℝ) (3/2),
         ‖angular r b D q-b‖ ≤ C*|q-1| ∧ ‖angularD r b D q‖ ≤ C := by
   …

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

2. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.compact_amplitude_jet_bound line 51

   Source documentation

   The finite C1 amplitude family has one bound on its compact parameter set; no incoming metric or regular-solution history occurs in this choice.

   lemma compact_amplitude_jet_bound {K : Set H} (hK : IsCompact K)
       (amps : Fin n → H → ℝ) (amps' : Fin n → H → H →L[ℝ] ℝ)
       (hc : ∀ j,ContinuousOn (amps j) K) (hd : ∀ j,ContinuousOn (amps' j) K) :
       ∃ U : ℝ,0 ≤ U ∧ ∀ x ∈ K,∀ j,|amps j x| ≤ U ∧ ‖amps' j x‖ ≤ U := by
   …

3. theorem OAI.HarmonicCounterexample.FiniteControl.SmoothWord.nonlinearBergerWord_uniform_C1_bound line 72

   Source documentation

   Quantitative compact-ball-ready C1 bounds for the nonlinear word on ALL of the time axis. The constants precede amplitudes, parameter jets, and duration.

   theorem nonlinearBergerWord_uniform_C1_bound (r : ℝ) (b : E) (D : Fin n → E) :
       ∃ C₀ C : ℝ,0 ≤ C₀ ∧ 0 ≤ C ∧
         ∀ (amps : Fin n → ℝ) (jets : Fin n → H →L[ℝ] ℝ) (U T : ℝ),
           0 ≤ U → (∀ j,|amps j| ≤ U) → (∀ j,‖jets j‖ ≤ U) →
           0 < T → 2*C₀*U ≤ T → ∀ t,
           ‖nonlinearBergerWord r b D amps T t-b‖ ≤ C*U/T ∧
           ‖∑ j : Fin n,((T⁻¹*duration n*bump j (duration n*t)) • jets j).smulRight
             (PulseTaylor.angularD r b (D j) (packetStretch amps T t j))‖ ≤ C*U/T := by
   …

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

4. theorem OAI.HarmonicCounterexample.FiniteControl.SmoothWord.insertWord_compact_C1_bound line 151

   Source documentation

   One parameter-ball bound for the actual inserted coefficient and its actual Frechet derivative. Both constants are fixed before ALL histories and time shifts.

   theorem insertWord_compact_C1_bound {K : Set H} (hK : IsCompact K)
       (r : ℝ) (b : E) (D : Fin n → E)
       (amps : Fin n → H → ℝ) (amps' : Fin n → H → H →L[ℝ] ℝ)
       (ha : ∀ x ∈ K,∀ j,HasFDerivAt (amps j) (amps' j x) x)
       (hc : ∀ j,ContinuousOn (amps j) K) (hd : ∀ j,ContinuousOn (amps' j) K) :
       ∃ T₀ C : ℝ,1 ≤ T₀ ∧ 0 ≤ C ∧ ∀ T ≥ T₀,∀ x ∈ K,
         (∀ j t,packetStretch (fun i => amps i x) T t j ∈ Icc (1/2:ℝ) (3/2)) ∧
         ∀ (history : ℝ → E) (α : ℝ → ℝ) (M a : ℝ),0 ≤ M →
           (∀ t,|α t| ≤ M) → ∀ t,
           ‖insertWord history α r b D (fun i => amps i x) a T t-history t‖ ≤ M*C/T ∧
           ‖fderiv ℝ (fun y => insertWord history α r b D (fun i => amps i y) a T t) x‖ ≤ M*C/T := by
   …

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

5. def OAI.HarmonicCounterexample.LinearODE.phaseCoefficientInjection line 212

   Source documentation

   Fixed continuous linear injection from angular coefficients to the lower-left phase block. It does not depend on histories or parameters.

   def phaseCoefficientInjection : (E →L[ℝ] E) →L[ℝ] OperatorPhase E →L[ℝ] OperatorPhase E :=
   …

   Mentions: OAI.HarmonicCounterexample.LinearODE.OperatorPhase

6. lemma OAI.HarmonicCounterexample.LinearODE.phaseCoefficientInjection_apply line 219
7. lemma OAI.HarmonicCounterexample.LinearODE.block_actual_fderiv_coeff line 223
8. lemma OAI.HarmonicCounterexample.LinearODE.block_actual_fderiv_smooth line 236
9. lemma OAI.HarmonicCounterexample.LinearODE.operator_phase_jet_norm_le line 247
10. lemma OAI.HarmonicCounterexample.LinearODE.block_actual_fderiv_norm line 258
11. theorem OAI.HarmonicCounterexample.LinearODE.actual_insertWord_compact_producer line 287

    Source documentation

    All global coefficient/phase regularity and bounds for a new pulse over a fixed compact parameter ball, produced by the actual Berger formula. The duration threshold precedes the incoming history and its time origin.

    theorem actual_insertWord_compact_producer {K : Set H} (hK : IsCompact K)
        (r B : ℝ) (D : Fin n → E →L[ℝ] E)
        (hD : ∀ j v,inner ℝ v (D j v) ≤ 0)
        (hBD : ∀ j v,-(B*‖v‖^2) ≤ inner ℝ v (D j v))
        (amps : Fin n → H → ℝ) (amps' : Fin n → H → H →L[ℝ] ℝ)
        (ha : ∀ x ∈ K,∀ j,HasFDerivAt (amps j) (amps' j x) x)
        (hc : ∀ j,ContinuousOn (amps j) K) (hd : ∀ j,ContinuousOn (amps' j) K) :
        ∃ T₀ C : ℝ,1 ≤ T₀ ∧ 0 ≤ C ∧ ∀ T ≥ T₀,
        ∀ (history : ℝ → E →L[ℝ] E) (α b : ℝ → ℝ) (M MH a : ℝ),
          ContDiff ℝ ∞ history → ContDiff ℝ ∞ α → 0 ≤ M → 0 ≤ MH →
          (∀ t,|α t| ≤ M) → (∀ t,‖history t‖ ≤ MH) →
          (∀ t v,0 ≤ inner ℝ v (history t v)) →
    …

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

12. theorem OAI.HarmonicCounterexample.LinearODE.selected_finite_berger_word_estimates line 386

    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 selected_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 ∧
          (∀ u j,j ≠ d u → bump j (duration n*u)=0 ∧ deriv (bump j) (duration n*u)=0) ∧
          (∀ 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) →
    …

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

13. theorem OAI.HarmonicCounterexample.LinearODE.compact_inserted_physical_estimates line 508

    Source documentation

    The actual smooth insertion satisfies all four physical value/ray error bounds, uniformly on a fixed compact parameter ball. Constants and duration thresholds precede incoming histories. All incoming jets are proved zero by causality, and all coefficient identities are obtained by differentiation.

    theorem compact_inserted_physical_estimates (basis : OrthonormalBasis ι ℝ E)
        {K : Set H} (hK : IsCompact K)
        (r B β p₀ θ γ M : ℝ) (D : Fin n → E →L[ℝ] E)
        (hD : ∀ j v,inner ℝ v (D j v) ≤ 0)
        (hBD : ∀ j v,-(B*‖v‖^2) ≤ inner ℝ v (D j v))
        (hM : 0 ≤ M) (hB : 0 ≤ B) (hθ : 0 ≤ θ) (hγ : 0 < γ)
        (hden : p₀+2*θ ≠ 0) (hroot : β*B-p₀*θ-θ^2=0)
        (amps : Fin n → H → ℝ) (amps' : Fin n → H → H →L[ℝ] ℝ)
        (ha : ∀ x ∈ K,∀ j,HasFDerivAt (amps j) (amps' j x) x)
        (hc : ∀ j,ContinuousOn (amps j) K) (hd : ∀ j,ContinuousOn (amps' j) K) :
        ∃ T₀ Z C : ℝ,1 ≤ T₀ ∧ 0 ≤ Z ∧ 1 ≤ C ∧ ∀ T ≥ T₀,
          ∀ (history : ℝ → E →L[ℝ] E) (α b : ℝ → ℝ) (MH Mb l B₀ a δ ε : ℝ),
    …

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

14. def OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketJet line 664

    Source documentation

    The actual Frechet derivative of the ideal packet, retained as a continuous linear map rather than only its finitely many rays.

    def unitPacketJet (a' : Fin n → H →L[ℝ] ℝ) (X : Fin n → E) (t : ℝ) : H →L[ℝ] E :=
    …

15. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketJet_smooth line 667
16. theorem OAI.HarmonicCounterexample.FiniteControl.SmoothWord.compact_ideal_packet_bound line 683

    Source documentation

    A single value-and-operator-jet bound on a compact parameter set, chosen before any physical history, duration or radial coefficients.

    theorem compact_ideal_packet_bound {K : Set H} (hK : IsCompact K)
        (amps : Fin n → H → ℝ) (amps' : Fin n → H → H →L[ℝ] ℝ)
        (hc : ∀ j,ContinuousOn (amps j) K) (hd : ∀ j,ContinuousOn (amps' j) K)
        (X : Fin n → E) :
        ∃ C : ℝ,0 ≤ C ∧ ∀ x ∈ K,
          (∀ t,‖unitPacketCoefficient (fun j => amps j x) X t‖ ≤ C) ∧
          (∀ t,‖unitPacketJet (fun j => amps' j x) X t‖ ≤ C) ∧
          (∫ t in (0:ℝ)..1,‖unitPacketCoefficient (fun j => amps j x) X t‖)+
            (∫ t in (0:ℝ)..1,‖unitPacketJet (fun j => amps' j x) X t‖) ≤ 2*C := by
    …

    Mentions: OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketCoefficient, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketJet

17. lemma OAI.HarmonicCounterexample.LinearODE.clipped_scalarBaseline_continuous line 744

    Source documentation

    Positive-time scalar baseline with a continuous global extension. This avoids making a false global nonsingularity claim at negative time.

    lemma clipped_scalarBaseline_continuous {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) {θ : ℝ} (hθ : 0 ≤ θ) (a : ℝ) :
        Continuous (fun t => scalarBaseline A p θ (max 0 (t-a))) := by
    …

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

18. theorem OAI.HarmonicCounterexample.LinearODE.compact_inserted_endpoint_C1 line 782

    Source documentation

    From the actual nonlinear coefficient producer and physical estimates to an actual normalized second-order transmission C1 estimate. Every error constant and duration threshold is chosen before the incoming history.

    theorem compact_inserted_endpoint_C1 (basis : OrthonormalBasis ι ℝ E)
        (hbasis : OrthonormalBasis κ ℝ H) {K : Set H} (hK : IsCompact K)
        (r B β p₀ θ γ M : ℝ) (D : Fin n → E →L[ℝ] E)
        (hD : ∀ j v,inner ℝ v (D j v) ≤ 0)
        (hBD : ∀ j v,-(B*‖v‖^2) ≤ inner ℝ v (D j v))
        (hM : 0 ≤ M) (hB : 0 ≤ B) (hθ : 0 ≤ θ) (hγ : 0 < γ)
        (hden : p₀+2*θ ≠ 0) (hroot : β*B-p₀*θ-θ^2=0)
        (amps : Fin n → H → ℝ) (amps' : Fin n → H → H →L[ℝ] ℝ)
        (ha : ∀ x ∈ K,∀ j,HasFDerivAt (amps j) (amps' j x) x)
        (hc : ∀ j,ContinuousOn (amps j) K) (hd : ∀ j,ContinuousOn (amps' j) K) :
        ∃ T₀ Z C J : ℝ,1 ≤ T₀ ∧ 0 ≤ Z ∧ 1 ≤ C ∧ 0 ≤ J ∧ ∀ T ≥ T₀,
          ∀ (history : ℝ → E →L[ℝ] E) (α b : ℝ → ℝ) (MH Mb l B₀ a δ ε : ℝ)
    …

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

19. theorem OAI.HarmonicCounterexample.LinearODE.actual_insertWord_differentiable line 933

    Source documentation

    Actual parameter differentiability of every center-regular value and slope for compactly supported smooth insertions. Bounds are local in parameter, not artificially global in the unbounded control space.

    theorem actual_insertWord_differentiable {K : Set H} (hK : IsCompact K)
        (r B : ℝ) (D : Fin n → E →L[ℝ] E)
        (hD : ∀ j v,inner ℝ v (D j v) ≤ 0)
        (hBD : ∀ j v,-(B*‖v‖^2) ≤ inner ℝ v (D j v))
        (amps : Fin n → H → ℝ) (amps' : Fin n → H → H →L[ℝ] ℝ)
        (ha : ∀ x ∈ K,∀ j,HasFDerivAt (amps j) (amps' j x) x)
        (hc : ∀ j,ContinuousOn (amps j) K) (hd : ∀ j,ContinuousOn (amps' j) K) :
        ∃ T₀ C : ℝ,1 ≤ T₀ ∧ 0 ≤ C ∧ ∀ T ≥ T₀,
        ∀ (history : ℝ → E →L[ℝ] E) (α b : ℝ → ℝ) (M MH Mb a l B₀ : ℝ)
          (S : Set H), IsOpen S → IsPreconnected S → S ⊆ K →
          ContDiff ℝ ∞ history → ContDiff ℝ ∞ α → Continuous b → 0 ≤ M → 0 ≤ MH → 0 ≤ Mb →
          (∀ t,|α t| ≤ M) → (∀ t,‖history t‖ ≤ MH) → (∀ t,|b t| ≤ Mb) →
    …

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

20. theorem OAI.HarmonicCounterexample.LinearODE.compact_inserted_outgoing_C1 line 1021
21. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.leftWord_differentiableAt line 1130
22. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.actual_packet_differentiableAt line 1138
23. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.leftWord_contDiff line 1149
24. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.actual_packet_contDiff line 1155
25. lemma OAI.HarmonicCounterexample.LinearODE.normalized_transmission_differentiableAt line 1177
26. lemma OAI.HarmonicCounterexample.LinearODE.small_radius_bounds line 1211
27. lemma OAI.HarmonicCounterexample.LinearODE.source_small_of_total line 1227
28. lemma OAI.HarmonicCounterexample.LinearODE.exponential_error_linear line 1237
29. theorem OAI.HarmonicCounterexample.LinearODE.compact_inserted_linear_C1 line 1246
30. lemma OAI.HarmonicCounterexample.LinearODE.linear_C1_error line 1353
31. def OAI.HarmonicCounterexample.LinearODE.orthogonalMatrixAlgHom line 1382
32. lemma OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix_exp line 1391
33. lemma OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix_leftWord line 1396
34. lemma OAI.HarmonicCounterexample.LinearODE.orthogonalMatrix_packet line 1405

    Source documentation

    Orthonormal coordinates of the genuine chronological ideal packet.

    lemma orthogonalMatrix_packet (b : OrthonormalBasis ι ℝ E) {n : ℕ}
        (a : Fin n → ℝ) (X : Fin n → E →L[ℝ] E) :
        orthogonalMatrix b (flow (fun t => ContinuousLinearMap.mul ℝ (E →L[ℝ] E)
          (unitPacketCoefficient a X t)) 1 1)=
          flow (fun t => ContinuousLinearMap.mul ℝ (Matrix ι ι ℝ)
            (unitPacketCoefficient a (fun j => orthogonalMatrix b (X j)) t)) 1 1 := by
    …

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

35. theorem OAI.HarmonicCounterexample.LinearODE.compact_inserted_matrix_C1 line 1443
36. lemma OAI.HarmonicCounterexample.LinearODE.pi_linear_difference_bound line 1517
37. theorem OAI.HarmonicCounterexample.LinearODE.finite_C1_error line 1528

    Source documentation

    Simultaneous finite-factor Frechet C1 control in the actual product norm.

    theorem finite_C1_error {f g : (i : β) → H → F i} {x : H} {η : ℝ}
        (hη : 0 ≤ η) (hf : ∀ i,DifferentiableAt ℝ (f i) x)
        (hg : ∀ i,DifferentiableAt ℝ (g i) x)
        (he : ∀ i,max ‖f i x-g i x‖ ‖fderiv ℝ (f i) x-fderiv ℝ (g i) x‖ ≤ η) :
        DifferentiableAt ℝ (fun y i => f i y) x ∧
          max ‖(fun i => f i x)-(fun i => g i x)‖
            ‖fderiv ℝ (fun y i => f i y) x-fderiv ℝ (fun y i => g i y) x‖ ≤ η := by
    …

38. lemma OAI.HarmonicCounterexample.LinearODE.finite_C1_norm line 1542