StripCompactSublevels.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The compact-sublevel property, with no regular-value or compactness premise, for stripTau and stripDomain.

lemma OAI.SymmetricMahler.stripTau_term_le line 14

theorem OAI.SymmetricMahler.strip_sublevel_coordinate_bound line 22

Source documentation

The coordinate bound using a closed disk of radius R^(1/(2m)).

theorem strip_sublevel_coordinate_bound (A : J → I → ℝ) {m : ℕ} (hm : 0 < m)
    {R : ℝ} (hR : 0 ≤ R) {z : (I → ℝ) × (I → ℝ)}
    (hz : z ∈ stripDomain A) (hτ : stripTau A m z ≤ R) (j : J) :
    stripCoordinate A z j ∈ F '' closedBall (0 : ℂ) (R ^ (2 * (m : ℝ))⁻¹) := by
…

Mentions: OAI.SymmetricMahler.stripDomain, OAI.SymmetricMahler.stripTau, OAI.SymmetricMahler.stripCoordinate

lemma OAI.SymmetricMahler.strip_radius_lt_one line 31
lemma OAI.SymmetricMahler.strip_disk_compact line 35
theorem OAI.SymmetricMahler.strip_sublevel_compact_container line 47
Source documentation
Rank gives a compact subset of U containing the closed R-sublevel. The compact set is the inverse image of the product of the F-images of closed disks.
```
theorem strip_sublevel_compact_container (A : J → I → ℝ)
    (hA : Function.Injective (measurement A)) {m : ℕ} (hm : 0 < m)
    {R : ℝ} (hR : 0 ≤ R) (hR1 : R < 1) :
    ∃ K : Set ((I → ℝ) × (I → ℝ)), IsCompact K ∧ K ⊆ stripDomain A ∧
      {z | z ∈ stripDomain A ∧ stripTau A m z ≤ R} ⊆ K := by
…
```
Mentions: OAI.SymmetricMahler.measurement, OAI.SymmetricMahler.stripDomain, OAI.SymmetricMahler.stripTau
theorem OAI.SymmetricMahler.strip_sublevel_compact_closure line 64
Source documentation
The compact-sublevel mass hypothesis holds for the finite-strip construction for every 0<R<1. Closure is ambient closure, and is contained in the open domain.
```
theorem strip_sublevel_compact_closure (A : J → I → ℝ)
    (hA : Function.Injective (measurement A)) {m : ℕ} (hm : 0 < m)
    {R : ℝ} (hR : 0 < R) (hR1 : R < 1) :
    IsCompact (closure {z | z ∈ stripDomain A ∧ stripTau A m z < R}) ∧
      closure {z | z ∈ stripDomain A ∧ stripTau A m z < R} ⊆ stripDomain A := by
…
```
Mentions: OAI.SymmetricMahler.measurement, OAI.SymmetricMahler.stripDomain, OAI.SymmetricMahler.stripTau