OAI/Analysis/Mahler/ConvexTransfer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SymmetricMahler.tendsto_volume_approximation line 11

   Source documentation

   Continuity from above applies to the actual decreasing strip bodies.

   theorem tendsto_volume_approximation {K : Set (I → ℝ)} (hK : IsCompact K)
       (hconv : Convex ℝ K) (hzero : (0 : I → ℝ) ∈ K) (hsym : ∀ x ∈ K, -x ∈ K)
       {c : ℝ} (hc : 0 < c) (hcK : ∀ i, Pi.single i c ∈ coordinatePolar K)
       (a : ℕ → coordinatePolar K) (ha : DenseRange a) :
       Tendsto (fun N => (volume (stripBody (approximationRows c (fun j => (a j).val) N))).toReal)
         atTop (𝓝 (volume K).toReal) := by
   …

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

2. theorem OAI.SymmetricMahler.arbitrary_body_bound_of_finite_strips line 24