OAI/Analysis/Mahler/ConvexSequence.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SymmetricMahler.prependPolarBasis line 11
2. lemma OAI.SymmetricMahler.prependPolarBasis_first line 15
3. lemma OAI.SymmetricMahler.prependPolarBasis_tail line 20
4. lemma OAI.SymmetricMahler.denseRange_prependPolarBasis line 25
5. lemma OAI.SymmetricMahler.linearIndependent_prependPolarBasis line 33

   Source documentation

   The first n terms of the sequence are linearly independent.

   lemma linearIndependent_prependPolarBasis (c : ℝ) (hc : c ≠ 0)
       (hcK : ∀ i : Fin n, Pi.single i c ∈ coordinatePolar K) (a : ℕ → coordinatePolar K) :
       LinearIndependent ℝ (fun i : Fin n => (prependPolarBasis c hcK a i).val) := by
   …

   Mentions: OAI.SymmetricMahler.coordinatePolar, OAI.SymmetricMahler.prependPolarBasis

6. lemma OAI.SymmetricMahler.prefix_stripBody_eq line 40

   Source documentation

   The literal first n+N rows describe exactly the previously constructed compact approximants.

   lemma prefix_stripBody_eq (c : ℝ) (hcK : ∀ i : Fin n, Pi.single i c ∈ coordinatePolar K)
       (a : ℕ → coordinatePolar K) (N : ℕ) :
       stripBody (fun j : Fin (n+N) => (prependPolarBasis c hcK a j).val) =
         stripBody (approximationRows c (fun j => (a j).val) N) := by
   …

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

7. theorem OAI.SymmetricMahler.exists_dense_polar_sequence line 68

   Source documentation

   Dense sequence with independent first rows exists for every compact set; no unproved polar-body theorem or density premise is supplied.

   theorem exists_dense_polar_sequence (hK : IsCompact K) :
       ∃ a : ℕ → coordinatePolar K, DenseRange a ∧
         LinearIndependent ℝ (fun i : Fin n => (a i).val) := by
   …

   Mentions: OAI.SymmetricMahler.coordinatePolar