OAI/Geometry/HarmonicGrowth/RealForms.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicCounterexample.RealForm.realImagEquiv line 26

   Source documentation

   The fixed real form of a conjugation really complexifies to the entire complex space; this is an actual linear equivalence, not a dimension assumption.

   def realImagEquiv : V ≃ₗ[ℝ] selfAdjoint V × selfAdjoint V where
   …

2. lemma OAI.HarmonicCounterexample.RealForm.real_form_finrank line 34
3. def OAI.HarmonicCounterexample.RealForm.complexCoordinates line 44
4. lemma OAI.HarmonicCounterexample.RealForm.complexCoordinates_injective line 56
5. lemma OAI.HarmonicCounterexample.RealForm.complexCoordinates_surjective line 69
6. def OAI.HarmonicCounterexample.RealForm.complexCoordinateEquiv line 85
7. def OAI.HarmonicCounterexample.RealForm.complexBasis line 91

   Source documentation

   A given real basis of the conjugation-fixed space is also a complex basis of the original complex space.

   def complexBasis (b : Basis ι ℝ (selfAdjoint V)) : Basis ι ℂ V :=
   …

   Mentions: OAI.HarmonicCounterexample.b

8. lemma OAI.HarmonicCounterexample.RealForm.complexBasis_apply line 94
9. def OAI.HarmonicCounterexample.RealForm.complexify line 129

   Source documentation

   Extension of a real endomorphism on the actual fixed real form.

   def complexify (T : Module.End ℝ (selfAdjoint V)) : Module.End ℂ V where
   …

10. lemma OAI.HarmonicCounterexample.RealForm.complexify_apply_fixed line 137
11. lemma OAI.HarmonicCounterexample.RealForm.complexify_realPart line 140
12. lemma OAI.HarmonicCounterexample.RealForm.complexify_imaginaryPart line 143
13. lemma OAI.HarmonicCounterexample.RealForm.complexify_injective line 146
14. lemma OAI.HarmonicCounterexample.RealForm.complexify_mul line 152
15. def OAI.HarmonicCounterexample.RealForm.complexifyLinear line 158

    Source documentation

    Complexification respects the REAL vector-space operations.

    def complexifyLinear : Module.End ℝ (selfAdjoint V) →ₗ[ℝ] Module.End ℂ V where
    …

16. lemma OAI.HarmonicCounterexample.RealForm.complexBasis_repr line 170
17. lemma OAI.HarmonicCounterexample.RealForm.complexify_matrix line 174
18. lemma OAI.HarmonicCounterexample.RealForm.complexify_trace line 180
19. lemma OAI.HarmonicCounterexample.RealForm.complexify_star line 211
20. def OAI.HarmonicCounterexample.RealForm.restrictReal line 223
21. lemma OAI.HarmonicCounterexample.RealForm.complexify_restrictReal line 226
22. def OAI.HarmonicCounterexample.RealForm.complexifyLie line 237
23. def OAI.HarmonicCounterexample.RealForm.complexifyTuple line 248
24. lemma OAI.HarmonicCounterexample.RealForm.complexifyTuple_injective line 255
25. lemma OAI.HarmonicCounterexample.RealForm.tuple_lieSpan_of_complexification line 262

    Source documentation

    Real simultaneous control descends to genuine endomorphisms of the fixed real spaces. This is an injective Lie-algebra descent, not a dimension assertion.

    lemma tuple_lieSpan_of_complexification {α : Type*}
        (G : α → ∀ i,Module.End ℝ (selfAdjoint (W i)))
        (X : ∀ i,Module.End ℝ (selfAdjoint (W i)))
        (h : complexifyTuple X ∈ LieSubalgebra.lieSpan ℝ _
            (Set.range (fun a => complexifyTuple (G a)))) :
        X ∈ LieSubalgebra.lieSpan ℝ _ (Set.range G) := by
    …

    Mentions: OAI.HarmonicCounterexample.RealForm.complexifyTuple, OAI.HarmonicCounterexample.a

26. instance OAI.HarmonicCounterexample.ComplexAngular.harmonicSpaceStar line 299

    Source documentation

    The real structure is Cartesian conjugation, i.e. coefficient conjugation combined with interchange of z and w in split complex coordinates.

    noncomputable instance harmonicSpaceStar (l : ℕ) : StarAddMonoid (harmonicSpace (Fin 8) l) where
    …

    Mentions: OAI.HarmonicCounterexample.ComplexAngular.harmonicSpace

27. instance OAI.HarmonicCounterexample.ComplexAngular.harmonicSpaceStarModule line 304
28. abbrev OAI.HarmonicCounterexample.ComplexAngular.realHarmonicSpace line 307
29. lemma OAI.HarmonicCounterexample.ComplexAngular.realHarmonicSpace_finrank line 309
30. lemma OAI.HarmonicCounterexample.ComplexAngular.harmonicEnd_star_of_conj line 313
31. lemma OAI.HarmonicCounterexample.ComplexAngular.complexify_harmonicEnd_conj line 321
32. def OAI.HarmonicCounterexample.Control.realHarmonicTupleGenerator line 354

    Source documentation

    Real generators on the actual real harmonic spaces, not formal matrix copies with an assumed complexification.

    def realHarmonicTupleGenerator (L : ℕ) (c : Fin L → ℝ)
        (J : ComplexStructure (Fin 8 ⊕ Fin 8)) :
        ∀ l : Fin L,Module.End ℝ (realHarmonicSpace (l.val+2)) :=
    …

33. lemma OAI.HarmonicCounterexample.Control.complexify_realHarmonicTupleGenerator line 359
34. theorem OAI.HarmonicCounterexample.Control.harmonic_simultaneous_actual_real line 369

    Source documentation

    Source simultaneous controllability, now on GENUINE real harmonic spaces with their actual real dimensions and actual real endomorphism traces.

    theorem harmonic_simultaneous_actual_real (L : ℕ) (c : Fin L → ℝ)
        (hc : ∀ l,c l ≠ 0)
        {X : ∀ l : Fin L,Module.End ℝ (realHarmonicSpace (l.val+2))}
        (hX : ∀ l,LinearMap.trace ℝ _ (X l)=0) :
        X ∈ LieSubalgebra.lieSpan ℝ _ (Set.range (realHarmonicTupleGenerator L c)) := by
    …

    Mentions: OAI.HarmonicCounterexample.Control.realHarmonicTupleGenerator