OAI/Analysis/Unitarizability/Average.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Dixmier.sum_pairwise_sq line 15

   Source documentation

   The finite Hilbert-space variance identity, without normalization.

   theorem sum_pairwise_sq (S : Finset I) (v : I → H) :
       ∑ i ∈ S, ∑ j ∈ S, ‖v i - v j‖ ^ 2 =
         2 * (S.card : ℝ) * (∑ i ∈ S, ‖v i‖ ^ 2) - 2 * ‖∑ i ∈ S, v i‖ ^ 2 := by
   …

2. theorem OAI.Dixmier.pairwise_sq_le_sum line 34

   Source documentation

   A chosen pair contributes at most the total squared defect.

   theorem pairwise_sq_le_sum (S : Finset I) (v : I → H) {i j : I}
       (hi : i ∈ S) (hj : j ∈ S) :
       ‖v i - v j‖ ^ 2 ≤ ∑ a ∈ S, ∑ b ∈ S, ‖v a - v b‖ ^ 2 := by
   …

3. theorem OAI.Dixmier.regular_sum_variance line 42

   Source documentation

   Defect in a finite sum of right translations of a unit vector.

   theorem regular_sum_variance (S : Finset G) (ξ : ScalarL2 G) (hξ : ‖ξ‖ = 1) :
       ∑ g ∈ S, ∑ h ∈ S, ‖rightRegular g ξ - rightRegular h ξ‖ ^ 2 =
         2 * ((S.card : ℝ) ^ 2 - ‖∑ g ∈ S, rightRegular g ξ‖ ^ 2) := by
   …

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

4. theorem OAI.Dixmier.exists_unit_near_opNorm line 50

   Source documentation

   A norm-one vector witnessing any strict lower bound for an operator norm.

   theorem exists_unit_near_opNorm (A : H →L[ℂ] H) {c : ℝ}
       (hc : 0 ≤ c) (hA : c < ‖A‖) : ∃ ξ : H, ‖ξ‖ = 1 ∧ c < ‖A ξ‖ := by
   …

5. theorem OAI.Dixmier.almost_invariant_of_sum_norm line 57

   Source documentation

   The norm-one-average hypothesis yields simultaneous almost invariance.

   theorem almost_invariant_of_sum_norm (S : Finset G) (h1 : (1 : G) ∈ S)
       (hS : ‖∑ g ∈ S, rightRegular g‖ = (S.card : ℝ))
       {ε : ℝ} (hε : 0 < ε) :
       ∃ ξ : ScalarL2 G, ‖ξ‖ = 1 ∧ ∀ g ∈ S, ‖rightRegular g ξ - ξ‖ < ε := by
   …

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