OAI/Analysis/Mahler/ConvexCompletion.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SymmetricMahler.convex_stripBody line 11
2. lemma OAI.SymmetricMahler.symmetric_stripBody line 29
3. lemma OAI.SymmetricMahler.stripBody_reindex line 34
4. lemma OAI.SymmetricMahler.measurement_reindex_injective line 44
5. theorem OAI.SymmetricMahler.arbitrary_body_bound_of_fin_matrices line 53

   Source documentation

   The arbitrary-body bound follows from finite-matrix bounds indexed by Fin N rows.

   theorem arbitrary_body_bound_of_fin_matrices {n : ℕ} {K : Set (Fin n → ℝ)}
       (hK : IsCompact K) (hconv : Convex ℝ K) (hsym : ∀ x ∈ K, -x ∈ K)
       (hint : (interior K).Nonempty) (C : ℝ)
       (hfinite : ∀ N (A : Fin N → Fin n → ℝ), Function.Injective (measurement A) →
         C ≤ (volume (stripBody A)).toReal * (volume (coordinatePolar (stripBody A))).toReal) :
       C ≤ (volume K).toReal * (volume (coordinatePolar K)).toReal := by
   …

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

6. theorem OAI.SymmetricMahler.symmetric_mahler_of_finite_strips line 65