OAI/RepresentationTheory/FiniteUnitary/KernelBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CubeShuffle.UnitaryFinite.actionKernel line 11
2. lemma OAI.CubeShuffle.UnitaryFinite.actionKernel_apply line 15
3. def OAI.CubeShuffle.UnitaryFinite.randomOperator line 34
4. lemma OAI.CubeShuffle.UnitaryFinite.coefficient_random line 38
5. def OAI.CubeShuffle.UnitaryFinite.fixedSpace line 56
6. theorem OAI.CubeShuffle.UnitaryFinite.operator_amplification line 65

   Source documentation

   Genuine multiplicity amplification: the family is produced from the stabilizer-fixed space by unitary Schur orthogonality, not assumed.

   theorem operator_amplification (a : G →* Equiv.Perm X) (x₀ : X)
       (ha : ∀ x, ∃ g, a g x₀=x) (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ]
       (hρ : IsUnitary ρ) (P : Ω → G)
       (hsym : ∀ x y, actionKernel a P x y=actionKernel a P y x)
       (hrow : ∀ x, ∑ y, actionKernel a P x y=1)
       (b z M : ℝ) (hb : 0≤b) (hz : 0<z) (hM0 : 0≤M)
       (hM : ∀ x, finiteMean (fun y => ((Fintype.card X:ℝ)*actionKernel a P x y)^(1+b)) ≤ M)
       (hm : 0 < Module.finrank ℂ (fixedSpace a x₀ ρ)) (v : V) (hv : ‖v‖=1) :
       ‖randomOperator ρ P v‖ ≤ M*z^(-b)+Real.sqrt (z/(Module.finrank ℂ (fixedSpace a x₀ ρ):ℝ)) := by
   …

   Mentions: OAI.CubeShuffle.UnitaryFinite.actionKernel, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.UnitaryFinite.fixedSpace, OAI.CubeShuffle.UnitaryFinite.randomOperator

7. lemma OAI.CubeShuffle.UnitaryFinite.sampleOperator_inv_apply line 101
8. theorem OAI.CubeShuffle.UnitaryFinite.sampleOperator_amplification line 107

   Source documentation

   FAC.7 as a genuine operator-norm bound for sample averages in an irrep.

   theorem sampleOperator_amplification (a : G →* Equiv.Perm X) (x₀ : X)
       (ha : ∀ x, ∃ g, a g x₀=x) (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ]
       (hρ : IsUnitary ρ) (P : Ω → G)
       (hsym : ∀ x y, actionKernel a P x y=actionKernel a P y x)
       (hrow : ∀ x, ∑ y, actionKernel a P x y=1)
       (b z M : ℝ) (hb : 0≤b) (hz : 0<z) (hM0 : 0≤M)
       (hM : ∀ x, finiteMean (fun y => ((Fintype.card X:ℝ)*actionKernel a P x y)^(1+b)) ≤ M)
       (hm : 0 < Module.finrank ℂ (fixedSpace a x₀ ρ)) :
       ‖sampleOperator ρ P‖ ≤ M*z^(-b)+Real.sqrt (z/(Module.finrank ℂ (fixedSpace a x₀ ρ):ℝ)) := by
   …

   Mentions: OAI.CubeShuffle.UnitaryFinite.actionKernel, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.UnitaryFinite.fixedSpace

9. def OAI.CubeShuffle.UnitaryFinite.subrepresentationEquiv line 123
10. lemma OAI.CubeShuffle.UnitaryFinite.irreducible_comp_equiv line 139