OAI/Analysis/SeparableQuotients/FiniteLp.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SeparableQuotient.LpFinite.array line 13

   Source documentation

   A rational array, as an ℓᵖ vector.

   def array (p : ℝ≥0∞) (f : Γ →₀ ℚ) : lp (fun _ : Γ => ℝ) p :=
   …

2. lemma OAI.SeparableQuotient.LpFinite.array_apply line 19
3. lemma OAI.SeparableQuotient.LpFinite.array_zero line 21
4. lemma OAI.SeparableQuotient.LpFinite.array_add line 26
5. lemma OAI.SeparableQuotient.LpFinite.array_smul line 31
6. lemma OAI.SeparableQuotient.LpFinite.array_sum line 37
7. lemma OAI.SeparableQuotient.LpFinite.norm_array_filter_le line 43
8. lemma OAI.SeparableQuotient.LpFinite.norm_array_single line 49
9. lemma OAI.SeparableQuotient.LpFinite.norm_sum_rpow line 67

   Source documentation

   Exact disjoint-support identity, including arbitrary finite index sets.

   lemma norm_sum_rpow (hp : 0 < p.toReal) (s : Finset ι)
       (v : ι → lp (fun _ : Γ => ℝ) p)
       (hdis : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → ∀ a, v i a = 0 ∨ v j a = 0) :
       ‖∑ i ∈ s, v i‖ ^ p.toReal = ∑ i ∈ s, ‖v i‖ ^ p.toReal := by
   …

10. lemma OAI.SeparableQuotient.LpFinite.norm_sum_le_card_rpow line 91
11. def OAI.SeparableQuotient.Norming.Family.r line 110
12. lemma OAI.SeparableQuotient.Norming.Family.r_gt_one line 111
13. lemma OAI.SeparableQuotient.Norming.Family.r_pos line 113
14. def OAI.SeparableQuotient.Norming.Family.exponent line 115
15. instance OAI.SeparableQuotient.Norming.Family.exponent_fact line 116
16. lemma OAI.SeparableQuotient.Norming.Family.exponent_toReal line 118
17. lemma OAI.SeparableQuotient.Norming.Family.exponent_ne_zero line 120
18. def OAI.SeparableQuotient.Norming.Family.theta line 123
19. lemma OAI.SeparableQuotient.Norming.Family.theta_nonneg line 124
20. lemma OAI.SeparableQuotient.Norming.Family.theta_formula line 126
21. lemma OAI.SeparableQuotient.Norming.TypeI.lp_bound line 129
22. lemma OAI.SeparableQuotient.Norming.FinitePath.crop_lp_bound line 160
23. lemma OAI.SeparableQuotient.Norming.TypeII.lp_bound line 189
24. lemma OAI.SeparableQuotient.Norming.Family.theta_le_one line 237
25. lemma OAI.SeparableQuotient.Norming.stage_lp_bound line 241
26. lemma OAI.SeparableQuotient.Norming.pure_lp_bound line 255

    Source documentation

    The pure coefficient ℓr estimate.

    lemma pure_lp_bound (k : ℕ) (x : Array) (hx : x ∈ Pure k) :
        ‖array (Family.pure k).exponent x‖ ≤ 1 := by
    …

    Mentions: OAI.SeparableQuotient.Norming.Array, OAI.SeparableQuotient.Norming.Pure