OAI/RepresentationTheory/FiniteUnitary/Averaging.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CubeShuffle.FiniteConvolution.conv line 9
2. def OAI.CubeShuffle.FiniteConvolution.power line 10
3. lemma OAI.CubeShuffle.FiniteConvolution.conv_nonneg line 14
4. lemma OAI.CubeShuffle.FiniteConvolution.conv_pos_of line 17
5. lemma OAI.CubeShuffle.FiniteConvolution.sum_conv line 24
6. lemma OAI.CubeShuffle.FiniteConvolution.power_nonneg line 33
7. lemma OAI.CubeShuffle.FiniteConvolution.sum_power line 39
8. lemma OAI.CubeShuffle.FiniteConvolution.power_list_pos line 45
9. lemma OAI.CubeShuffle.FiniteConvolution.power_pos_mono line 54
10. theorem OAI.CubeShuffle.FiniteConvolution.exists_positive_power line 63

    Source documentation

    Finite generation and a positive holding probability produce a genuine finite-time positive minorant, rather than a spectral-gap assumption.

    theorem exists_positive_power {p : G → ℝ} (hp : ∀ g, 0 ≤ p g) (h1 : 0 < p 1)
        (hgen : Subgroup.closure {g | 0 < p g}=⊤) :
        ∃ n : ℕ, ∀ g, 0 < power p (2^n) g := by
    …

    Mentions: OAI.CubeShuffle.FiniteConvolution.power

11. structure OAI.CubeShuffle.FiniteConvolution.Minorant line 78
12. def OAI.CubeShuffle.FiniteConvolution.minorant line 85
13. def OAI.CubeShuffle.UnitaryFinite.continuousRepresentation line 107

    Distinct definitions of this name: ComparatorChallenges/WeightedSweepMoments.lean:239 (same statement text; different proof or body). Qualify references as OAI.CubeShuffle.UnitaryFinite.continuousRepresentation@path.

14. lemma OAI.CubeShuffle.UnitaryFinite.continuousRepresentation_apply line 113
15. lemma OAI.CubeShuffle.UnitaryFinite.unitary_norm line 117
16. lemma OAI.CubeShuffle.UnitaryFinite.continuousRepresentation_norm_le line 122
17. lemma OAI.CubeShuffle.UnitaryFinite.continuousRepresentation_adjoint line 129
18. def OAI.CubeShuffle.UnitaryFinite.weightedOperator line 137
19. lemma OAI.CubeShuffle.UnitaryFinite.weightedOperator_norm_le line 140
20. lemma OAI.CubeShuffle.UnitaryFinite.weightedOperator_symmetric line 148
21. def OAI.CubeShuffle.UnitaryFinite.uniformOperator line 158
22. lemma OAI.CubeShuffle.UnitaryFinite.uniformOperator_symmetric line 161
23. lemma OAI.CubeShuffle.UnitaryFinite.uniformOperator_left line 164
24. lemma OAI.CubeShuffle.UnitaryFinite.uniformOperator_right line 171
25. lemma OAI.CubeShuffle.UnitaryFinite.uniformOperator_idempotent line 178
26. lemma OAI.CubeShuffle.UnitaryFinite.uniformOperator_projection line 187
27. lemma OAI.CubeShuffle.UnitaryFinite.weighted_uniform_left line 191
28. lemma OAI.CubeShuffle.UnitaryFinite.weighted_uniform_right line 198
29. theorem OAI.CubeShuffle.UnitaryFinite.doeblin_off_invariants line 207

    Source documentation

    A finite Doeblin minorant gives a dimension-free contraction off invariants; no irreducible decomposition or unproved spectral-gap hypothesis is used.

    theorem doeblin_off_invariants (ρ : Representation ℂ G V) (hρ : IsUnitary ρ)
        (p : G → ℝ) (hp : ∑ g,p g=1) (ε : ℝ)
        (hminor : ∀ g, ε/(Fintype.card G:ℝ)≤p g) :
        ‖weightedOperator ρ p * (1-uniformOperator ρ)‖≤1-ε := by
    …

    Mentions: OAI.CubeShuffle.UnitaryFinite.weightedOperator, OAI.CubeShuffle.UnitaryFinite.uniformOperator

30. lemma OAI.CubeShuffle.UnitaryFinite.weightedOperator_conv line 243
31. lemma OAI.CubeShuffle.UnitaryFinite.weightedOperator_power line 256
32. lemma OAI.CubeShuffle.UnitaryFinite.off_invariants_pow line 262
33. def OAI.CubeShuffle.UnitaryFinite.minorantGap line 278

    Source documentation

    Explicit gap from the finite-time minorant; its value depends only on the finite group law, not on the dimension of any represented space.

    noncomputable def minorantGap {p : G → ℝ} (c : FiniteConvolution.Minorant p) : ℝ :=
    …

    Mentions: OAI.CubeShuffle.FiniteConvolution.Minorant

34. lemma OAI.CubeShuffle.UnitaryFinite.minorantGap_pos line 282
35. lemma OAI.CubeShuffle.UnitaryFinite.minorantGap_lt_one line 291
36. theorem OAI.CubeShuffle.UnitaryFinite.norm_off_invariants_le_gap line 297

    Source documentation

    The one-block strict contraction follows from generation and the genuine holding probability via Doeblin; this is uniform over ALL unitary representations.

    theorem norm_off_invariants_le_gap (ρ : Representation ℂ G V) (hρ : IsUnitary ρ)
        (p : G → ℝ) (hp : ∑ g,p g=1) (hsym : ∀ g,p g⁻¹=p g)
        (c : FiniteConvolution.Minorant p) :
        ‖weightedOperator ρ p-uniformOperator ρ‖ ≤ minorantGap c := by
    …

    Mentions: OAI.CubeShuffle.FiniteConvolution.Minorant, OAI.CubeShuffle.UnitaryFinite.weightedOperator, OAI.CubeShuffle.UnitaryFinite.uniformOperator, OAI.CubeShuffle.UnitaryFinite.minorantGap

37. def OAI.CubeShuffle.FiniteAverage.orderedProduct line 330
38. lemma OAI.CubeShuffle.FiniteAverage.orderedProduct_eq line 334
39. lemma OAI.CubeShuffle.FiniteAverage.multilinear_average line 350
40. lemma OAI.CubeShuffle.FiniteAverage.ordered_average line 357

    Source documentation

    Exact independence factorization for commuting finite random factors.

    lemma ordered_average (x : I → Ω → A)
        (hc : ∀ ω, Pairwise fun i j => Commute (x i (ω i)) (x j (ω j)))
        (havg : Pairwise fun i j => Commute ((Fintype.card Ω:ℂ)⁻¹ • ∑ ω,x i ω)
          ((Fintype.card Ω:ℂ)⁻¹ • ∑ ω,x j ω)) :
        (Finset.univ.noncommProd (fun i => (Fintype.card Ω:ℂ)⁻¹ • ∑ ω,x i ω)
          (fun _ _ _ _ hij => havg hij))=
        (Fintype.card (I → Ω):ℂ)⁻¹ • ∑ ω : I → Ω,
          Finset.univ.noncommProd (fun i => x i (ω i)) (fun _ _ _ _ hij => hc ω hij) := by
    …