OAI/Analysis/Mahler/ConvexMain.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SymmetricMahler.measurement_prefix_injective line 10
2. theorem OAI.SymmetricMahler.exists_finite_strip_approximation line 26

   Source documentation

   An approximation certificate for an arbitrary symmetric convex body. The sequence and every geometric and measure property are constructed from exactly the body hypotheses; no approximation premise remains. Each prefix has N+n rows and contains the independent first n rows.

   theorem exists_finite_strip_approximation (_hn : 1 ≤ n) (hK : IsCompact K)
       (hconv : Convex ℝ K) (hsym : ∀ x ∈ K, -x ∈ K) (hint : (interior K).Nonempty) :
       ∃ a : ℕ → coordinatePolar K,
         DenseRange a ∧
         LinearIndependent ℝ (fun i : Fin n => (a i).val) ∧
         (∀ N, Function.Injective (measurement (fun j : Fin (n+N) => (a j).val))) ∧
         (∀ N, IsCompact (stripBody (fun j : Fin (n+N) => (a j).val)) ∧
           Convex ℝ (stripBody (fun j : Fin (n+N) => (a j).val)) ∧
           (∀ x ∈ stripBody (fun j : Fin (n+N) => (a j).val),
             -x ∈ stripBody (fun j : Fin (n+N) => (a j).val)) ∧
           (interior (stripBody (fun j : Fin (n+N) => (a j).val))).Nonempty) ∧
         Antitone (fun N => stripBody (fun j : Fin (n+N) => (a j).val)) ∧
   …

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