OAI/Analysis/Unitarizability/VectorMean.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Dixmier.summable_l2_sq line 14
2. def OAI.Dixmier.vectorMeanValue line 17
3. theorem OAI.Dixmier.vectorMean_summable line 20
4. theorem OAI.Dixmier.vectorMean_norm_le line 27
5. def OAI.Dixmier.vectorMeanLinear line 40
6. def OAI.Dixmier.vectorMean line 51
7. theorem OAI.Dixmier.vectorMean_apply line 54
8. theorem OAI.Dixmier.vectorMean_one line 57
9. theorem OAI.Dixmier.vectorMean_opNorm_le line 62
10. theorem OAI.Dixmier.vectorMean_positive line 65
11. theorem OAI.Dixmier.vectorMean_translate line 77
12. theorem OAI.Dixmier.norm_sq_difference_le line 84
13. theorem OAI.Dixmier.l2_square_difference_bound line 97

    Source documentation

    The l2-to-l1 estimate behind the vector-mean translation error bound.

    theorem l2_square_difference_bound (ξ η : ScalarL2 G) :
        Summable (fun x => |‖ξ x‖^2 - ‖η x‖^2|) ∧
        (∑' x, |‖ξ x‖^2 - ‖η x‖^2|) ≤ ‖ξ - η‖ * (‖ξ‖ + ‖η‖) := by
    …

    Mentions: OAI.Dixmier.ScalarL2

14. theorem OAI.Dixmier.vectorMean_difference_bound line 118
15. theorem OAI.Dixmier.vectorMean_translation_bound line 146

    Source documentation

    The vector-mean translation error estimate.

    theorem vectorMean_translation_bound [DiscreteTopology G] (ξ : ScalarL2 G) (hξ : ‖ξ‖ = 1)
        (g : G) (b : G →ᵇ ℂ) :
        ‖vectorMean ξ (leftTranslate g b) - vectorMean ξ b‖ ≤
          2 * ‖b‖ * ‖rightRegular g⁻¹ ξ - ξ‖ := by
    …

    Mentions: OAI.Dixmier.ScalarL2, OAI.Dixmier.vectorMean, OAI.Dixmier.leftTranslate, OAI.Dixmier.rightRegular