StripSublevelTopology.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Topological and rank properties of the finite-strip sublevels. No differential, Jacobian or change-of-variables result is assumed.

def OAI.SymmetricMahler.measurementLinear line 15
theorem OAI.SymmetricMahler.measurement_full_rank_iff line 22
Source documentation
The rank-n premise is exactly injectivity of measurement.
```
theorem measurement_full_rank_iff [Fintype J] (A : J → I → ℝ) :
    Module.finrank ℝ (LinearMap.range (measurementLinear A)) = Fintype.card I ↔
      Function.Injective (measurement A) := by
…
```
Mentions: OAI.SymmetricMahler.measurementLinear, OAI.SymmetricMahler.measurement
lemma OAI.SymmetricMahler.stripTau_eq_sum_pow line 35
theorem OAI.SymmetricMahler.stripTau_eq_sum_norm_sq line 42
Source documentation
The literal tau is exactly the squared Euclidean norm of the displayed holomorphic vector f_j = h((Az)_j)^m, expressed as a coordinate sum.
```
theorem stripTau_eq_sum_norm_sq (A : J → I → ℝ) (m : ℕ)
    (z : (I → ℝ) × (I → ℝ)) :
    stripTau A m z = ∑ j, ‖inverseF (stripCoordinate A z j) ^ m‖ ^ 2 := by
…
```
Mentions: OAI.SymmetricMahler.stripTau, OAI.SymmetricMahler.stripCoordinate
lemma OAI.SymmetricMahler.stripGeometry_continuousOn_tau line 47
theorem OAI.SymmetricMahler.isOpen_strip_sublevel line 58
Source documentation
Every strict sublevel is open in the ambient real 2n-space.
```
theorem isOpen_strip_sublevel (A : J → I → ℝ) (m : ℕ) (R : ℝ) :
    IsOpen {z | z ∈ stripDomain A ∧ stripTau A m z < R} := by
…
```
Mentions: OAI.SymmetricMahler.stripDomain, OAI.SymmetricMahler.stripTau
theorem OAI.SymmetricMahler.isCompact_strip_closed_sublevel line 68
Source documentation
Closed R-sublevels are themselves compact for R<1, not merely bounded.
```
theorem isCompact_strip_closed_sublevel (A : J → I → ℝ)
    (hA : Function.Injective (measurement A)) {m : ℕ} (hm : 0 < m)
    {R : ℝ} (hR : 0 ≤ R) (hR1 : R < 1) :
    IsCompact {z | z ∈ stripDomain A ∧ stripTau A m z ≤ R} := by
…
```
Mentions: OAI.SymmetricMahler.measurement, OAI.SymmetricMahler.stripDomain, OAI.SymmetricMahler.stripTau