StripRankGeometry.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SymmetricMahler.stripCoordinateLinear line 13
Source documentation
The complexification of the real strip matrix, in real pair coordinates.
```
def stripCoordinateLinear (A : J → I → ℝ) :
    ((I → ℝ) × (I → ℝ)) →ₗ[ℝ] (J → ℂ) where
…
```
lemma OAI.SymmetricMahler.stripCoordinate_injective line 22
lemma OAI.SymmetricMahler.continuous_stripCoordinate line 36
theorem OAI.SymmetricMahler.stripCoordinate_isClosedEmbedding line 40
Source documentation
Rank n implies properness of the full complexified matrix.
```
theorem stripCoordinate_isClosedEmbedding (A : J → I → ℝ)
    (hA : Function.Injective (measurement A)) :
    Topology.IsClosedEmbedding (stripCoordinate A) :=
…
```
Mentions: OAI.SymmetricMahler.measurement, OAI.SymmetricMahler.stripCoordinate
theorem OAI.SymmetricMahler.stripCoordinate_compact_preimage line 47
Source documentation
Compact coordinate constraints have compact inverse image, with no additional boundedness assumption on z.
```
theorem stripCoordinate_compact_preimage (A : J → I → ℝ)
    (hA : Function.Injective (measurement A)) {K : Set (J → ℂ)} (hK : IsCompact K) :
    IsCompact (stripCoordinate A ⁻¹' K) :=
…
```
Mentions: OAI.SymmetricMahler.measurement, OAI.SymmetricMahler.stripCoordinate
lemma OAI.SymmetricMahler.stripCoordinate_zero line 53
lemma OAI.SymmetricMahler.stripCoordinate_eq_zero_iff line 56
lemma OAI.SymmetricMahler.stripGeometry_isOpen_domain line 62
lemma OAI.SymmetricMahler.zero_mem_stripDomain line 69
theorem OAI.SymmetricMahler.strip_power_common_zero line 76
Source documentation
The literal holomorphic map used in the mass application has only the origin as a common zero.
```
theorem strip_power_common_zero (A : J → I → ℝ)
    (hA : Function.Injective (measurement A)) {m : ℕ} (hm : 0 < m)
    {z : (I → ℝ) × (I → ℝ)} (hz : z ∈ stripDomain A) :
    (∀ j, inverseF (stripCoordinate A z j) ^ m = 0) ↔ z = 0 := by
…
```
Mentions: OAI.SymmetricMahler.measurement, OAI.SymmetricMahler.stripDomain, OAI.SymmetricMahler.stripCoordinate

theorem OAI.SymmetricMahler.strip_leading_common_zero line 89

Source documentation

The displayed leading homogeneous map also has no nonzero common zero.

theorem strip_leading_common_zero (A : J → I → ℝ)
    (hA : Function.Injective (measurement A)) {m : ℕ} (hm : 0 < m)
    {c : ℂ} (hc : c ≠ 0) {z : (I → ℝ) × (I → ℝ)} :
    (∀ j, (c * stripCoordinate A z j) ^ m = 0) ↔ z = 0 := by
…

Mentions: OAI.SymmetricMahler.measurement, OAI.SymmetricMahler.stripCoordinate