OAI/Analysis/SeparableQuotients/MarkedEstimates.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SeparableQuotient.FiniteVectors.vec line 12
2. lemma OAI.SeparableQuotient.FiniteVectors.vec_apply line 14
3. lemma OAI.SeparableQuotient.FiniteVectors.vec_zero line 15
4. lemma OAI.SeparableQuotient.FiniteVectors.vec_add line 16
5. lemma OAI.SeparableQuotient.FiniteVectors.vec_smul line 17
6. lemma OAI.SeparableQuotient.FiniteVectors.norm_rpow line 19
7. lemma OAI.SeparableQuotient.FiniteVectors.norm_le line 24
8. lemma OAI.SeparableQuotient.FiniteVectors.sum_rpow_larger line 30
9. lemma OAI.SeparableQuotient.FiniteVectors.norm_mono_exponent line 51
10. lemma OAI.SeparableQuotient.FiniteVectors.norm_const line 56
11. lemma OAI.SeparableQuotient.FiniteVectors.norm_le_card line 63
12. lemma OAI.SeparableQuotient.FiniteVectors.norm_mask_le line 70
13. lemma OAI.SeparableQuotient.FiniteVectors.norm_eq_rpow line 83
14. lemma OAI.SeparableQuotient.FiniteVectors.sum_abs_le_norm line 87
15. lemma OAI.SeparableQuotient.FiniteVectors.marked_norm_bound line 103

    Source documentation

    Eight marked entries per row imply the precise uniform marked charge, using only the actual column Hölder bound.

    lemma marked_norm_bound (q : ℝ) (hq : 1 < q) (r : ℝ≥0∞) (hqr : q ≤ r.toReal)
        (a : β → ℝ) (ha : ∑ b, |a b|^q ≤ 1) (marks : β → Finset ι)
        (hmarks : ∀ b, (marks b).card ≤ 8) (M : ι → ℝ) (hM : ∀ i, 0 ≤ M i)
        (hcolumn : ∀ i, M i ≤ 2 * (∑ b, if i ∈ marks b then |a b|^q else 0)^(1/q)) :
        ‖vec r M‖ ≤ 16 ∧ ∑ i, M i ≤ 16*(Fintype.card ι : ℝ)^(1-1/q) := by
    …

    Mentions: OAI.SeparableQuotient.FiniteVectors.vec

16. def OAI.SeparableQuotient.ActualSpace.ThinnedWindows.markedCharge line 152
17. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.markedCharge_nonneg line 157
18. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.marked_column line 165
19. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.marked_vector_bounds line 190