FiniteStripReduction.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SymmetricMahler.StripMassBound line 12
theorem OAI.SymmetricMahler.finite_strip_product_of_mass line 19
Source documentation
Finite-m normalization and polar-volume bound. Construction, Jacobian, change-of-variables and image estimates follow from the hypotheses; the only analytic premise is the mass lower bound.
```
theorem finite_strip_product_of_mass (A : Matrix (Fin N) (Fin n) ℝ)
    (hA : Function.Injective (measurement A)) {m : ℕ} (hm : 2 ≤ m)
    (hmass : StripMassBound A m) :
    ENNReal.ofReal ((4 : ℝ)^n/(Nat.factorial n : ℝ)) ≤
      ENNReal.ofReal ((1+(N : ℝ)*planarError m)^n)*
        (volume (stripBody A)*volume (coordinatePolar (stripBody A))) := by
…
```
Mentions: OAI.SymmetricMahler.measurement, OAI.SymmetricMahler.StripMassBound, OAI.SymmetricMahler.planarError, OAI.SymmetricMahler.stripBody, OAI.SymmetricMahler.coordinatePolar
theorem OAI.SymmetricMahler.finite_strip_mahler_of_mass line 52
Source documentation
The finite-strip symmetric Mahler inequality follows from the exact isolated-zero mass bound. No finiteness assumption on either volume is needed for this extended-nonnegative-real formulation.
```
theorem finite_strip_mahler_of_mass (A : Matrix (Fin N) (Fin n) ℝ)
    (hA : Function.Injective (measurement A))
    (hmass : ∀ m : ℕ, 2 ≤ m → StripMassBound A m) :
    ENNReal.ofReal ((4 : ℝ)^n/(Nat.factorial n : ℝ)) ≤
      volume (stripBody A)*volume (coordinatePolar (stripBody A)) := by
…
```
Mentions: OAI.SymmetricMahler.measurement, OAI.SymmetricMahler.StripMassBound, OAI.SymmetricMahler.stripBody, OAI.SymmetricMahler.coordinatePolar