OAI/Analysis/SeparableQuotients/RealCoefficients.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SeparableQuotient.RealCoefficients.rational_to_real line 16

   Source documentation

   Rational coefficients suffice for the closed finite-dimensional ℓq ball. This uses actual density, not an assumed real Type II operation.

   lemma rational_to_real (q : ℝ) (hq : 0 < q) (v : ι → Z)
       (h : ∀ c : ι → ℚ, (∑ i, |(c i : ℝ)| ^ q) ≤ 1 → ‖∑ i, (c i : ℝ) • v i‖ ≤ 1)
       (c : ι → ℝ) (hc : (∑ i, |c i| ^ q) ≤ 1) : ‖∑ i, c i • v i‖ ≤ 1 := by
   …

2. lemma OAI.SeparableQuotient.RealCoefficients.bound_from_unit line 75
3. def OAI.SeparableQuotient.RealCoefficients.signChoice line 110
4. lemma OAI.SeparableQuotient.RealCoefficients.abs_signChoice line 112
5. lemma OAI.SeparableQuotient.RealCoefficients.signChoice_mul line 116