OAI/Analysis/Mahler/ComplexStripMap.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SymmetricMahler.complexToReal line 12
2. def OAI.SymmetricMahler.realToComplex line 15
3. lemma OAI.SymmetricMahler.realToComplex_complexToReal line 18
4. lemma OAI.SymmetricMahler.complexToReal_realToComplex line 22
5. def OAI.SymmetricMahler.complexRealLinearEquiv line 26
6. def OAI.SymmetricMahler.complexRealEquiv line 34
7. lemma OAI.SymmetricMahler.volume_preserving_complexToReal line 39

   Source documentation

   The explicit separation of real and imaginary coordinates preserves standard Lebesgue measure exactly, with no normalization factor.

   lemma volume_preserving_complexToReal : MeasurePreserving (complexToReal (n := n)) := by
   …

   Mentions: OAI.SymmetricMahler.complexToReal

8. def OAI.SymmetricMahler.complexRow line 45
9. lemma OAI.SymmetricMahler.complexRow_apply line 48
10. lemma OAI.SymmetricMahler.complexRow_re line 51
11. lemma OAI.SymmetricMahler.complexRow_im line 55
12. lemma OAI.SymmetricMahler.complexRow_eq_stripCoordinate line 59
13. def OAI.SymmetricMahler.complexStripDomain line 63
14. lemma OAI.SymmetricMahler.complexStripDomain_eq_preimage line 66
15. lemma OAI.SymmetricMahler.isOpen_complexStripDomain line 71
16. lemma OAI.SymmetricMahler.zero_mem_complexStripDomain line 75
17. def OAI.SymmetricMahler.specialMap line 79
18. theorem OAI.SymmetricMahler.differentiableOn_specialMap line 83

    Source documentation

    The holomorphic map used in the mass inequality.

    theorem differentiableOn_specialMap (A : Matrix (Fin N) (Fin n) ℝ) (m : ℕ) :
        DifferentiableOn ℂ (specialMap A m) (complexStripDomain A) := by
    …

    Mentions: OAI.SymmetricMahler.specialMap, OAI.SymmetricMahler.complexStripDomain

19. lemma OAI.SymmetricMahler.complexRow_injective line 92
20. theorem OAI.SymmetricMahler.specialMap_eq_zero_iff line 108

    Source documentation

    The actual map has precisely one common zero on its actual domain.

    theorem specialMap_eq_zero_iff (A : Matrix (Fin N) (Fin n) ℝ)
        (hA : Function.Injective (measurement A)) {m : ℕ} (hm : 0 < m)
        {z : Fin n → ℂ} (hz : z ∈ complexStripDomain A) : specialMap A m z = 0 ↔ z = 0 := by
    …

    Mentions: OAI.SymmetricMahler.measurement, OAI.SymmetricMahler.complexStripDomain, OAI.SymmetricMahler.specialMap