RegularMassReduction.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SymmetricMahler.SpecialRegularMassBound line 13
Source documentation
The regular-level mass bound for the finite-strip map.
```
def SpecialRegularMassBound {N n : ℕ} (A : Matrix (Fin N) (Fin n) ℝ) (m k : ℕ) : Prop :=
…
```

theorem OAI.SymmetricMahler.symmetric_mahler_from_regular_special_mass line 20

Source documentation

The full body inequality follows from regular-level mass estimates for the actual special maps alone. General Sard and a general mass theorem are not needed by this reduction.

theorem symmetric_mahler_from_regular_special_mass {n : ℕ} (hn : 1 ≤ n)
    (hmass : ∀ N (A : Matrix (Fin N) (Fin n) ℝ), Function.Injective (measurement A) →
      ∀ m : ℕ, 2 ≤ m → ∀ k, SpecialRegularMassBound A m k)
    {K : Set (Fin n → ℝ)} (hK : IsCompact K) (hconv : Convex ℝ K)
    (hsym : ∀ x ∈ K, -x ∈ K) (hint : (interior K).Nonempty) :
    (4 : ℝ)^n/(Nat.factorial n : ℝ) ≤
      (volume K).toReal*(volume (coordinatePolar K)).toReal := by
…

Mentions: OAI.SymmetricMahler.measurement, OAI.SymmetricMahler.SpecialRegularMassBound, OAI.SymmetricMahler.coordinatePolar