OAI/Geometry/HarmonicGrowth/ControlWords.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicCounterexample.FiniteControl.expUnit line 15
2. lemma OAI.HarmonicCounterexample.FiniteControl.expUnit_val line 17
3. lemma OAI.HarmonicCounterexample.FiniteControl.expUnit_inv_val line 20
4. def OAI.HarmonicCounterexample.FiniteControl.adjoint line 23
5. lemma OAI.HarmonicCounterexample.FiniteControl.adjoint_apply line 29
6. lemma OAI.HarmonicCounterexample.FiniteControl.adjoint_one line 33
7. lemma OAI.HarmonicCounterexample.FiniteControl.adjoint_mul line 36
8. lemma OAI.HarmonicCounterexample.FiniteControl.adjoint_lie line 41
9. lemma OAI.HarmonicCounterexample.FiniteControl.adjoint_exp_deriv line 46
10. lemma OAI.HarmonicCounterexample.FiniteControl.deriv_mem_submodule line 57
11. def OAI.HarmonicCounterexample.FiniteControl.reachable line 75
12. def OAI.HarmonicCounterexample.FiniteControl.adjointSpan line 78
13. lemma OAI.HarmonicCounterexample.FiniteControl.generator_mem_adjointSpan line 81
14. lemma OAI.HarmonicCounterexample.FiniteControl.adjoint_mem_adjointSpan line 84
15. lemma OAI.HarmonicCounterexample.FiniteControl.generator_lie_adjointSpan line 94
16. lemma OAI.HarmonicCounterexample.FiniteControl.adjoint_inv_cancel line 102
17. lemma OAI.HarmonicCounterexample.FiniteControl.adjointSpan_lie_mem line 105
18. theorem OAI.HarmonicCounterexample.FiniteControl.lieSpan_le_adjointSpan line 122

    Source documentation

    Differentiating ACTUAL reachable conjugations, in a closed finite -dimensional span, proves the spanning assertion used for finite words.

    theorem lieSpan_le_adjointSpan [FiniteDimensional ℝ A] (g : κ → A) :
        (LieSubalgebra.lieSpan ℝ A (Set.range g)).toSubmodule ≤ adjointSpan g := by
    …

    Mentions: OAI.HarmonicCounterexample.FiniteControl.adjointSpan

19. theorem OAI.HarmonicCounterexample.FiniteControl.exists_adjoint_basis line 145

    Source documentation

    A finite basis of actual reachable conjugates, as opposed to abstract iterated brackets or a closure of the reachable subgroup.

    theorem exists_adjoint_basis [FiniteDimensional ℝ A] (g : κ → A) :
        ∃ (d : ℕ) (b : Module.Basis (Fin d) ℝ (adjointSpan g)),
          ∀ i,∃ (h : Aˣ),h ∈ reachable g ∧ ∃ k,(b i : A)=adjoint h (g k) := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.FiniteControl.adjointSpan, OAI.HarmonicCounterexample.FiniteControl.reachable, OAI.HarmonicCounterexample.FiniteControl.adjoint

20. lemma OAI.HarmonicCounterexample.FiniteControl.strict_deriv_conjugate line 186
21. lemma OAI.HarmonicCounterexample.FiniteControl.adjoint_unit line 199
22. lemma OAI.HarmonicCounterexample.FiniteControl.prod_at_zero line 203
23. lemma OAI.HarmonicCounterexample.FiniteControl.strict_deriv_identity_product line 210
24. theorem OAI.HarmonicCounterexample.FiniteControl.conjugate_word_differential line 228

    Source documentation

    The finite conjugation word has the required exact differential, calculated in the actual Banach algebra, not postulated as a control hypothesis.

    theorem conjugate_word_differential [FiniteDimensional ℝ A] {d : ℕ}
        (h : Fin d → Aˣ) (X : Fin d → A) :
        HasStrictFDerivAt
          (fun t : Fin d → ℝ => ((List.finRange d).map
            (fun i => adjoint (h i) (NormedSpace.exp (t i • X i)))).prod)
          (∑ i : Fin d,(ContinuousLinearMap.proj i : (Fin d → ℝ) →L[ℝ] ℝ).smulRight (adjoint (h i) (X i))) 0 := by
    …

    Mentions: OAI.HarmonicCounterexample.FiniteControl.adjoint

25. def OAI.HarmonicCounterexample.FiniteControl.conjugateWord line 254
26. lemma OAI.HarmonicCounterexample.FiniteControl.conjugateWord_zero line 258
27. lemma OAI.HarmonicCounterexample.FiniteControl.conjugateWord_smooth line 265
28. theorem OAI.HarmonicCounterexample.FiniteControl.exists_word_submersion line 280

    Source documentation

    The ACTUAL finite word assembled from reachable conjugates has an invertible differential onto its adjoint span. If Lie generation is full this is exactly the finite-word submersion at the group identity.

    theorem exists_word_submersion [FiniteDimensional ℝ A] (g : κ → A) :
        ∃ (d : ℕ) (h : Fin d → Aˣ) (k : Fin d → κ)
          (e : (Fin d → ℝ) ≃L[ℝ] (adjointSpan g)),
          (∀ i,h i ∈ reachable g) ∧
          d=Module.finrank ℝ (adjointSpan g) ∧
          ContDiff ℝ ∞ (conjugateWord h (g ∘ k)) ∧
          HasStrictFDerivAt (conjugateWord h (g ∘ k))
            ((adjointSpan g).subtypeL.comp (e : (Fin d → ℝ) →L[ℝ] (adjointSpan g))) 0 := by
    …

    Mentions: OAI.HarmonicCounterexample.FiniteControl.adjointSpan, OAI.HarmonicCounterexample.FiniteControl.reachable, OAI.HarmonicCounterexample.FiniteControl.conjugateWord

29. def OAI.HarmonicCounterexample.FiniteControl.conjugateWordUnit line 318
30. lemma OAI.HarmonicCounterexample.FiniteControl.conjugateWordUnit_val line 321
31. lemma OAI.HarmonicCounterexample.FiniteControl.conjugateWordUnit_mem line 327
32. theorem OAI.HarmonicCounterexample.FiniteControl.reachable_open_of_adjointSpan_top line 338

    Source documentation

    Full linear span is promoted to an ACTUAL open reachable subgroup by the strict inverse/submersion theorem. No topological closure of reachability is used.

    theorem reachable_open_of_adjointSpan_top [FiniteDimensional ℝ A] (g : κ → A)
        (hfull : adjointSpan g=⊤) : IsOpen (reachable g : Set Aˣ) := by
    …

    Mentions: OAI.HarmonicCounterexample.FiniteControl.adjointSpan, OAI.HarmonicCounterexample.FiniteControl.reachable

33. theorem OAI.HarmonicCounterexample.FiniteControl.reachable_open_of_lieSpan_top line 364
34. lemma OAI.HarmonicCounterexample.FiniteControl.expUnit_neg line 381
35. lemma OAI.HarmonicCounterexample.FiniteControl.reachable_has_word line 385
36. lemma OAI.HarmonicCounterexample.FiniteControl.word_reachable line 406
37. lemma OAI.HarmonicCounterexample.FiniteControl.single_product line 425
38. lemma OAI.HarmonicCounterexample.FiniteControl.diag2n_decompose line 431
39. lemma OAI.HarmonicCounterexample.FiniteControl.transvection_induction line 445

    Source documentation

    Every real or arbitrary-field special-linear matrix has a finite elementary transvection word. This avoids assuming polar decomposition or connectedness.

    lemma transvection_induction [Nontrivial ι] (P : Matrix.SpecialLinearGroup ι F → Prop)
        (htransvec : ∀ (i j : ι) (hij : i ≠ j) (a : F),P (transvection hij a))
        (hmul : ∀ A B,P A → P B → P (A*B)) (M : Matrix.SpecialLinearGroup ι F) : P M := by
    …

    Mentions: OAI.HarmonicCounterexample.a

40. lemma OAI.HarmonicCounterexample.FiniteControl.continuous_transvection line 468
41. lemma OAI.HarmonicCounterexample.FiniteControl.joined_transvection line 480
42. lemma OAI.HarmonicCounterexample.FiniteControl.sl_joined_one line 484
43. theorem OAI.HarmonicCounterexample.FiniteControl.sl_pathConnected line 494

    Source documentation

    Actual path connectedness of every nontrivial real special linear group, proved by finite elementary operations, without any polar decomposition axiom.

    theorem sl_pathConnected [Nontrivial ι] : PathConnectedSpace (Matrix.SpecialLinearGroup ι ℝ) := by
    …

44. abbrev OAI.HarmonicCounterexample.FiniteControl.MatrixProduct line 514
45. def OAI.HarmonicCounterexample.FiniteControl.centralMatrix line 516
46. lemma OAI.HarmonicCounterexample.FiniteControl.centralMatrix_zero line 519
47. lemma OAI.HarmonicCounterexample.FiniteControl.centralMatrix_add line 523
48. lemma OAI.HarmonicCounterexample.FiniteControl.centralMatrix_neg line 527
49. lemma OAI.HarmonicCounterexample.FiniteControl.centralMatrix_commute line 531
50. lemma OAI.HarmonicCounterexample.FiniteControl.expUnit_add_commute line 536
51. lemma OAI.HarmonicCounterexample.FiniteControl.central_expUnit_commute line 542
52. def OAI.HarmonicCounterexample.FiniteControl.augmented line 547
53. lemma OAI.HarmonicCounterexample.FiniteControl.augmented_lieSpan_top line 553
54. lemma OAI.HarmonicCounterexample.FiniteControl.augmented_reachable_split line 576
55. def OAI.HarmonicCounterexample.FiniteControl.slProductToUnits line 616

    Source documentation

    The ordinary product of REAL SL groups has a continuous genuine embedding into units of the product matrix algebra.

    def slProductToUnits : (∀ b,Matrix.SpecialLinearGroup (ι b) ℝ) →* (MatrixProduct ι)ˣ where
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.FiniteControl.MatrixProduct

56. lemma OAI.HarmonicCounterexample.FiniteControl.slProductToUnits_continuous line 626
57. def OAI.HarmonicCounterexample.FiniteControl.detMultilinear line 647
58. lemma OAI.HarmonicCounterexample.FiniteControl.hasDerivAt_det line 650
59. lemma OAI.HarmonicCounterexample.FiniteControl.hasDerivAt_det_leftODE line 658
60. lemma OAI.HarmonicCounterexample.FiniteControl.hasDerivAt_exp_row line 670
61. lemma OAI.HarmonicCounterexample.FiniteControl.hasDerivAt_det_exp line 683
62. theorem OAI.HarmonicCounterexample.FiniteControl.matrix_det_exp line 689

    Source documentation

    Liouville's formula for the ACTUAL real matrix exponential.

    theorem matrix_det_exp (X : Matrix ι ι ℝ) :
        (NormedSpace.exp X).det=Real.exp X.trace := by
    …

63. lemma OAI.HarmonicCounterexample.FiniteControl.reachable_tracefree_det line 722
64. lemma OAI.HarmonicCounterexample.FiniteControl.slProduct_augmented_reachable line 744
65. theorem OAI.HarmonicCounterexample.FiniteControl.slProduct_reachable line 763

    Source documentation

    Lie generation of the actual trace-free product implies exact finite-word reachability in the genuine product of real special-linear groups. The proof uses ambient submersion only; central augmentation is eliminated by determinants.

    theorem slProduct_reachable [∀ b,Nontrivial (ι b)]
        (g : κ → MatrixProduct ι) (hg : ∀ k b,(g k b).trace=0)
        (hfull : ∀ X : MatrixProduct ι,(∀ b,(X b).trace=0) →
          X ∈ LieSubalgebra.lieSpan ℝ _ (Set.range g))
        (M : ∀ b,Matrix.SpecialLinearGroup (ι b) ℝ) :
        slProductToUnits M ∈ reachable g := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.FiniteControl.MatrixProduct, OAI.HarmonicCounterexample.FiniteControl.slProductToUnits, OAI.HarmonicCounterexample.FiniteControl.reachable

66. theorem OAI.HarmonicCounterexample.FiniteControl.slProduct_has_finite_word line 786
67. def OAI.HarmonicCounterexample.FiniteControl.tracefreeProduct line 810
68. lemma OAI.HarmonicCounterexample.FiniteControl.adjoint_trace line 816
69. lemma OAI.HarmonicCounterexample.FiniteControl.adjointSpan_eq_tracefree line 824
70. theorem OAI.HarmonicCounterexample.FiniteControl.sl_target_word_submersion line 840

    Source documentation

    A genuine smooth finite control word centered at ANY desired special-linear product, with an isomorphic derivative onto the right-translated trace-free space. Every conjugating factor is itself an actual finite control word.

    theorem sl_target_word_submersion [∀ b,Nontrivial (ι b)]
        (g : κ → MatrixProduct ι) (hg : ∀ k b,(g k b).trace=0)
        (hfull : ∀ X : MatrixProduct ι,(∀ b,(X b).trace=0) →
          X ∈ LieSubalgebra.lieSpan ℝ _ (Set.range g))
        (M : ∀ b,Matrix.SpecialLinearGroup (ι b) ℝ) :
        ∃ (d : ℕ) (h : Fin d → (MatrixProduct ι)ˣ) (k : Fin d → κ)
          (e : (Fin d → ℝ) ≃L[ℝ] (tracefreeProduct (ι:=ι)))
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.FiniteControl.MatrixProduct, OAI.HarmonicCounterexample.FiniteControl.tracefreeProduct

71. def OAI.HarmonicCounterexample.FiniteControl.parameterWord line 873

    Source documentation

    A finite control word with genuine smooth scalar amplitudes.

    def parameterWord (g : κ → A) (w : List (κ × (H → ℝ))) (x : H) : A :=
    …

72. def OAI.HarmonicCounterexample.FiniteControl.constantWord line 876
73. def OAI.HarmonicCounterexample.FiniteControl.inverseWord line 879
74. lemma OAI.HarmonicCounterexample.FiniteControl.parameterWord_append line 883
75. lemma OAI.HarmonicCounterexample.FiniteControl.constantWord_value line 888
76. lemma OAI.HarmonicCounterexample.FiniteControl.inverseWord_value line 896
77. lemma OAI.HarmonicCounterexample.FiniteControl.constantWord_smooth line 902
78. theorem OAI.HarmonicCounterexample.FiniteControl.conjugate_word_flatten line 910

    Source documentation

    Flatten reachable conjugations and the target into one fixed finite list. No abstract exponential controls remain beyond the permitted generators.

    theorem conjugate_word_flatten {d : ℕ} (g : κ → A)
        (h : Fin d → Aˣ) (k : Fin d → κ) (w : Fin d → List (κ × ℝ))
        (hw : ∀ i,(w i |>.map (fun p => expUnit (p.2 • g p.1))).prod=h i)
        (target : List (κ × ℝ)) (coord : H →L[ℝ] (Fin d → ℝ)) :
        ∃ z : List (κ × (H → ℝ)),
          (∀ p ∈ z,ContDiff ℝ ∞ p.2) ∧
          ∀ x,parameterWord g z x=conjugateWord h (g ∘ k) (coord x)*
            ((target.map (fun p => expUnit (p.2 • g p.1))).prod : Aˣ) := by
    …

    Mentions: OAI.HarmonicCounterexample.FiniteControl.expUnit, OAI.HarmonicCounterexample.FiniteControl.parameterWord, OAI.HarmonicCounterexample.FiniteControl.conjugateWord

79. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.leftWord_reverse_product line 963
80. lemma OAI.HarmonicCounterexample.FiniteControl.SmoothWord.packet_reverse_list line 973
81. theorem OAI.HarmonicCounterexample.FiniteControl.SmoothWord.smooth_packet_of_parameter_word line 991

    Source documentation

    The finite SL word is realized by the actual smooth chronological packet, with a positive number of slots and smooth genuine amplitudes.

    theorem smooth_packet_of_parameter_word [Nonempty κ] (g : κ → A)
        (w : List (κ × (H → ℝ))) (hw : ∀ p ∈ w,ContDiff ℝ ∞ p.2) :
        ∃ (n : ℕ) (_ : NeZero n) (slot : Fin n → κ) (amps : Fin n → H → ℝ),
          (∀ i,ContDiff ℝ ∞ (amps i)) ∧ ∀ x,
          LinearODE.flow (fun t => ContinuousLinearMap.mul ℝ A
            (unitPacketCoefficient (fun i => amps i x) (fun i => g (slot i)) t)) 1 1=
              parameterWord g w x := by
    …

    Mentions: OAI.HarmonicCounterexample.LinearODE.flow, OAI.HarmonicCounterexample.FiniteControl.SmoothWord.unitPacketCoefficient, OAI.HarmonicCounterexample.FiniteControl.parameterWord

82. abbrev OAI.HarmonicCounterexample.FiniteControl.Frobenius.MatrixProduct' line 1027
83. def OAI.HarmonicCounterexample.FiniteControl.Frobenius.tracefreeProduct' line 1029
84. def OAI.HarmonicCounterexample.FiniteControl.Frobenius.meanTrace line 1035
85. def OAI.HarmonicCounterexample.FiniteControl.Frobenius.tracefreeProjection line 1040

    Source documentation

    Linear local SL chart: project away scalar matrices after translating the exact target to the identity. No abstract manifold chart is assumed.

    def tracefreeProjection : MatrixProduct' (ι:=ι) →ₗ[ℝ] tracefreeProduct' (ι:=ι) where
    …

    Mentions: OAI.HarmonicCounterexample.FiniteControl.Frobenius.MatrixProduct', OAI.HarmonicCounterexample.FiniteControl.Frobenius.tracefreeProduct'

86. lemma OAI.HarmonicCounterexample.FiniteControl.Frobenius.tracefreeProjection_zero_iff line 1061

    Source documentation

    Projection zero is exactly scalarity, with the scalar given explicitly.

    lemma tracefreeProjection_zero_iff (X : MatrixProduct' (ι:=ι)) :
    …

    Mentions: OAI.HarmonicCounterexample.FiniteControl.Frobenius.MatrixProduct'

87. lemma OAI.HarmonicCounterexample.FiniteControl.Frobenius.tracefreeProjection_id line 1073
88. lemma OAI.HarmonicCounterexample.FiniteControl.Frobenius.tracefreeProjection_subtype line 1079
89. lemma OAI.HarmonicCounterexample.FiniteControl.Frobenius.positive_scalar_of_projection_zero line 1088

    Source documentation

    Positivity of trace resolves the spurious negative scalar branch. This is an OPEN condition near the prescribed positive scalar times the target.

    lemma positive_scalar_of_projection_zero {X : MatrixProduct' (ι:=ι)}
    …

    Mentions: OAI.HarmonicCounterexample.FiniteControl.Frobenius.MatrixProduct'

90. lemma OAI.HarmonicCounterexample.FiniteControl.Frobenius.exact_scalar_target line 1097

    Source documentation

    Vanishing projected transmission gives the EXACT target, up to the positive scalar permitted by source equation (exact-transmission).

    lemma exact_scalar_target {X : MatrixProduct' (ι:=ι)} (M : (MatrixProduct' (ι:=ι))ˣ)
    …

    Mentions: OAI.HarmonicCounterexample.FiniteControl.Frobenius.MatrixProduct'

91. def OAI.HarmonicCounterexample.FiniteControl.Frobenius.translatedProjection line 1124
92. lemma OAI.HarmonicCounterexample.FiniteControl.Frobenius.translatedProjection_apply line 1129
93. lemma OAI.HarmonicCounterexample.FiniteControl.Frobenius.positive_trace_neighborhood line 1133
94. theorem OAI.HarmonicCounterexample.FiniteControl.Frobenius.uniform_exact_scalar_attainment line 1163

    Source documentation

    Quantitative actual exact positive-scalar attainment, avoiding determinant normalization altogether. Each actual map has genuine Frechet derivatives and uniform C1 errors; the same tolerance works for every preceding history.

    theorem uniform_exact_scalar_attainment
        (M : (MatrixProduct' (ι:=ι))ˣ) (Φ : E → MatrixProduct' (ι:=ι))
    …

    Mentions: OAI.HarmonicCounterexample.FiniteControl.Frobenius.MatrixProduct'

95. def OAI.HarmonicCounterexample.FiniteControl.Frobenius.boundedScalarNeighborhood line 1210
96. lemma OAI.HarmonicCounterexample.FiniteControl.Frobenius.boundedScalarNeighborhood_open line 1213
97. lemma OAI.HarmonicCounterexample.FiniteControl.Frobenius.bounded_scalar_target line 1231
98. theorem OAI.HarmonicCounterexample.FiniteControl.Frobenius.uniform_exact_bounded_scalar_attainment line 1251

    Source documentation

    The exact target scalar stays in a fixed compact positive range. This also supplies the uniform logarithmic scalar bound required for growth.

    theorem uniform_exact_bounded_scalar_attainment
        (M : (MatrixProduct' (ι:=ι))ˣ) (Φ : E → MatrixProduct' (ι:=ι))
    …

    Mentions: OAI.HarmonicCounterexample.FiniteControl.Frobenius.MatrixProduct'

99. theorem OAI.HarmonicCounterexample.FiniteControl.Frobenius.whole_period_uniform_attainment line 1305

    Source documentation

    Uniform actual WHOLE-period attainment, after factoring the entire parameter-independent diagonal leg. The error tolerance is chosen before K, Q and B, so it does not depend on the incoming history or diagonal anisotropy. Q and B have genuine Frechet derivatives.

    theorem whole_period_uniform_attainment
        (M : (MatrixProduct' (ι:=ι))ˣ) (Φ : E → MatrixProduct' (ι:=ι))
    …

    Mentions: OAI.HarmonicCounterexample.FiniteControl.Frobenius.MatrixProduct'

100. lemma OAI.HarmonicCounterexample.FiniteControl.Frobenius.whole_period_exact_leg line 1373

     Source documentation

     Cancellation of the factor of the ENTIRE diagonal leg gives the exact chronological target c D M. No exponentially anisotropic conjugation occurs.

     lemma whole_period_exact_leg {U V P B : MatrixProduct' (ι:=ι)} {θ : ℝ}
     …

     Mentions: OAI.HarmonicCounterexample.FiniteControl.Frobenius.MatrixProduct'

101. theorem OAI.HarmonicCounterexample.FiniteControl.smooth_SL_packet_submersion line 1409

     Source documentation

     The actual smooth chronological finite control packet centered at the exact SL target, with a genuine invertible projected derivative. The parameter norm is Euclidean, the same norm used by the uniform physical estimates.

     theorem smooth_SL_packet_submersion (g : κ → MatrixProduct ι)
         (hg : ∀ k b,(g k b).trace=0)
         (hfull : ∀ X : MatrixProduct ι,(∀ b,(X b).trace=0) →
           X ∈ LieSubalgebra.lieSpan ℝ _ (Set.range g))
         (M : ∀ b,Matrix.SpecialLinearGroup (ι b) ℝ) :
         ∃ (d n : ℕ) (_ : NeZero n) (slot : Fin n → κ)
           (amps : Fin n → EuclideanSpace ℝ (Fin d) → ℝ)
           (A : EuclideanSpace ℝ (Fin d) ≃L[ℝ] tracefreeProduct' (ι:=ι)),
     …

     Mentions: OAI.HarmonicCounterexample.FiniteControl.MatrixProduct, OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.FiniteControl.tracefreeProduct'