StripLevelGeometry.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Positive levels of the literal strip tau are the compact boundaries of its strict sublevels. This supplies set geometry, not boundary-chart integration.

theorem OAI.SymmetricMahler.isCompact_strip_level line 15

Source documentation

The actual level set is compact in the ambient real 2n-space.

theorem isCompact_strip_level (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

theorem OAI.SymmetricMahler.frontier_strip_sublevel line 37

Source documentation

The boundary used in Stokes is exactly tau=R, with no boundary-identification premise.

theorem frontier_strip_sublevel (A : J → I → ℝ)
    (hA : Function.Injective (measurement A)) {m : ℕ} (hm : 0 < m)
    {R : ℝ} (hR : 0 < R) (hR1 : R < 1) :
    frontier {z | z ∈ stripDomain A ∧ stripTau A m z < R} =
      {z | z ∈ stripDomain A ∧ stripTau A m z = R} := by
…

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