OAI/Analysis/SeparableQuotients/LpDuality.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SeparableQuotient.LpCoding.finite line 13
2. lemma OAI.SeparableQuotient.LpCoding.finite_apply line 18
3. lemma OAI.SeparableQuotient.LpCoding.finite_single line 20
4. lemma OAI.SeparableQuotient.LpCoding.norm_finite line 26
5. lemma OAI.SeparableQuotient.LpCoding.finite_dense line 35
6. lemma OAI.SeparableQuotient.LpCoding.finite_dual_bound line 45

   Source documentation

   The finite-support formulation of the norm of an ℓp dual element.

   lemma finite_dual_bound (hpq : p.toReal.HolderConjugate q.toReal)
       (C : ℝ) (hC : 0 ≤ C) (a : ι → ℝ)
       (h : ∀ c : ι →₀ ℝ, |c.sum (fun i t => t*a i)| ≤ C*‖finite p c‖)
       (s : Finset ι) : ∑ i ∈ s, |a i| ^ q.toReal ≤ C ^ q.toReal := by
   …

   Mentions: OAI.SeparableQuotient.LpCoding.finite

7. lemma OAI.SeparableQuotient.LpCoding.dual_mem line 100
8. lemma OAI.SeparableQuotient.LpCoding.dual_norm line 106
9. lemma OAI.SeparableQuotient.LpCoding.single_eq_smul line 122
10. lemma OAI.SeparableQuotient.LpCoding.coefficient_bound line 126
11. def OAI.SeparableQuotient.LpCoding.coefficients line 138
12. lemma OAI.SeparableQuotient.LpCoding.coefficients_apply line 144
13. lemma OAI.SeparableQuotient.LpCoding.norm_coefficients_le line 149
14. def OAI.SeparableQuotient.LpCoding.coefficientMap line 153
15. lemma OAI.SeparableQuotient.LpCoding.coefficientMap_apply line 161
16. lemma OAI.SeparableQuotient.LpCoding.norm_coefficientMap_le line 165
17. lemma OAI.SeparableQuotient.LpCoding.eval_coefficients_symm line 173

    Source documentation

    Symmetry of the two ℓp dual evaluations.

    lemma eval_coefficients_symm (hpq : p.toReal.HolderConjugate q.toReal)
        (hp : p ≠ ∞) (hq : q ≠ ∞)
        (g : StrongDual ℝ (lp (fun _ : ι => ℝ) p))
        (h : StrongDual ℝ (lp (fun _ : ι => ℝ) q)) :
        g (coefficients hpq.symm h) = h (coefficients hpq g) := by
    …

    Mentions: OAI.SeparableQuotient.LpCoding.coefficients

18. def OAI.SeparableQuotient.LpCoding.analysisMap line 195
19. lemma OAI.SeparableQuotient.LpCoding.analysisMap_apply line 204
20. lemma OAI.SeparableQuotient.LpCoding.norm_analysisMap_le line 208