StripRegularValues.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Regular positive levels of the literal strip tau. This specializes the regular-value step to the actual conformal map; it is not a general Sard theorem.

lemma OAI.SymmetricMahler.stripTau_eq_sum_normSq_pow line 15
lemma OAI.SymmetricMahler.stripCoordinate_real_smul line 21
def OAI.SymmetricMahler.stripTauRadialSlope line 28
theorem OAI.SymmetricMahler.hasDerivAt_stripTau_radial line 33
theorem OAI.SymmetricMahler.stripTauRadialSlope_pos line 43
theorem OAI.SymmetricMahler.differentiableAt_stripTau line 61
theorem OAI.SymmetricMahler.stripTau_positive_regular line 87
Source documentation
Every positive value of the actual tau is regular. The derivative is surjective onto the real scalars, the standard regular-value condition.
```
theorem stripTau_positive_regular (A : J → I → ℝ)
    (hA : Function.Injective (measurement A)) {m : ℕ} (hm : 0 < m)
    {R : ℝ} (hR : 0 < R) {z : (I → ℝ) × (I → ℝ)}
    (hz : z ∈ stripDomain A) (hlevel : stripTau A m z = R) :
    Function.Surjective (fderiv ℝ (stripTau A m) z) := by
…
```
Mentions: OAI.SymmetricMahler.measurement, OAI.SymmetricMahler.stripDomain, OAI.SymmetricMahler.stripTau