SpecialMassHypotheses.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SymmetricMahler.specialTau line 13
Source documentation
Squared Euclidean norm of the actual holomorphic vector, in coordinates.
```
noncomputable def specialTau (A : Matrix (Fin N) (Fin n) ℝ) (m : ℕ) (z : Fin n → ℂ) : ℝ :=
…
```
lemma OAI.SymmetricMahler.specialTau_eq_stripTau line 16

theorem OAI.SymmetricMahler.specialTau_compact_closure line 22

Source documentation

The compact-closure premise transfers to actual complex coordinates.

theorem specialTau_compact_closure (A : Matrix (Fin N) (Fin n) ℝ)
    (hA : Function.Injective (measurement A)) {m : ℕ} (hm : 0 < m)
    {R : ℝ} (hR : 0 < R) (hR1 : R < 1) :
    IsCompact (closure {z | z ∈ complexStripDomain A ∧ specialTau A m z < R}) ∧
      closure {z | z ∈ complexStripDomain A ∧ specialTau A m z < R} ⊆ complexStripDomain A := by
…

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

theorem OAI.SymmetricMahler.specialMap_mass_hypotheses line 46