OAI/Analysis/NuclearUltrapower/Kazhdan.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.NuclearUltrapower.SOS.ElementarySpectral.vectorStabilizer line 15
2. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.deltaOp_ker_fixed line 28
3. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.exists_fixed_nearby line 48

   Source documentation

   The constructive quantitative projection consequence actually used in the semidirect-product proof. It does not assume a Kazhdan pair.

   theorem exists_fixed_nearby (ρ : E →* (H ≃ₗᵢ[ℂ] H)) (x : H) :
       ∃ y : H, (∀ g : E, ρ g y = y) ∧
         (1/10 : ℝ) * ‖x-y‖ ^ 2 ≤ SOSEnergy.energy eGenSet ρ x := by
   …

   Mentions: OAI.NuclearUltrapower.SOS.E, OAI.NuclearUltrapower.SOSEnergy.energy, OAI.NuclearUltrapower.SOS.eGenSet

4. def OAI.NuclearUltrapower.Elementary.integralAction line 76
5. abbrev OAI.NuclearUltrapower.Elementary.IntegralGroup line 81
6. def OAI.NuclearUltrapower.Elementary.integralTranslation line 83
7. def OAI.NuclearUltrapower.Elementary.integralTheta line 86
8. theorem OAI.NuclearUltrapower.Elementary.integralTheta_left line 98
9. theorem OAI.NuclearUltrapower.Elementary.integralTheta_right line 101
10. theorem OAI.NuclearUltrapower.Elementary.integralTheta_injective line 104
11. theorem OAI.NuclearUltrapower.Elementary.integralTheta_translation line 114
12. theorem OAI.NuclearUltrapower.Elementary.integralTheta_pow_translation line 117
13. def OAI.NuclearUltrapower.Elementary.integralInclusion line 127

    Source documentation

    The inclusion is literally integer coordinate inclusion into Z[1/2].

    def integralInclusion : IntegralGroup →* G where
    …

    Mentions: OAI.NuclearUltrapower.Elementary.IntegralGroup, OAI.NuclearUltrapower.G

14. def OAI.NuclearUltrapower.Elementary.stableLetter line 141

    Source documentation

    The stable letter t=(0,I,1).

    def stableLetter : G :=
    …

    Mentions: OAI.NuclearUltrapower.G

15. theorem OAI.NuclearUltrapower.Elementary.stableLetter_conjugation line 145

    Source documentation

    The source group law implements exactly multiplication of translations by two.

    theorem stableLetter_conjugation (g : IntegralGroup) :
        stableLetter * integralInclusion g * stableLetter⁻¹ = integralInclusion (integralTheta g) := by
    …

    Mentions: OAI.NuclearUltrapower.Elementary.IntegralGroup, OAI.NuclearUltrapower.Elementary.stableLetter, OAI.NuclearUltrapower.Elementary.integralInclusion, OAI.NuclearUltrapower.Elementary.integralTheta

16. theorem OAI.NuclearUltrapower.Elementary.integralInclusion_injective line 161

    Source documentation

    The integral copy is genuinely a subgroup, not merely a homomorphic image.

    theorem integralInclusion_injective : Function.Injective integralInclusion := by
    …

    Mentions: OAI.NuclearUltrapower.Elementary.integralInclusion

17. abbrev OAI.NuclearUltrapower.Elementary.Residue3 line 173
18. def OAI.NuclearUltrapower.Elementary.residue line 175
19. def OAI.NuclearUltrapower.Elementary.residueMatrix line 177
20. theorem OAI.NuclearUltrapower.Elementary.residue_mul line 180
21. theorem OAI.NuclearUltrapower.Elementary.residue_one line 186
22. theorem OAI.NuclearUltrapower.Elementary.residue_theta line 188
23. theorem OAI.NuclearUltrapower.Elementary.mem_theta_range_iff line 194
24. theorem OAI.NuclearUltrapower.Elementary.leftRel_theta_iff line 211
25. def OAI.NuclearUltrapower.Elementary.thetaCosetEquiv line 225

    Source documentation

    The eight left cosets are precisely the three translation residues.

    def thetaCosetEquiv : (IntegralGroup ⧸ integralTheta.range) ≃ Residue3 where
    …

    Mentions: OAI.NuclearUltrapower.Elementary.IntegralGroup, OAI.NuclearUltrapower.Elementary.Residue3

26. theorem OAI.NuclearUltrapower.Elementary.integralTheta_index line 238
27. instance OAI.NuclearUltrapower.Elementary.(instance at line 242) line 242
28. def OAI.NuclearUltrapower.Elementary.residuePermutation line 245

    Source documentation

    Reduction modulo two, acting by affine permutations on its eight points.

    def residuePermutation : IntegralGroup →* Equiv.Perm Residue3 where
    …

    Mentions: OAI.NuclearUltrapower.Elementary.IntegralGroup, OAI.NuclearUltrapower.Elementary.Residue3

29. theorem OAI.NuclearUltrapower.Elementary.residuePermutation_apply line 257
30. abbrev OAI.NuclearUltrapower.Elementary.ResidueHilbert line 260
31. def OAI.NuclearUltrapower.Elementary.residueUnitary line 262
32. theorem OAI.NuclearUltrapower.Elementary.residueUnitary_apply line 276
33. def OAI.NuclearUltrapower.Elementary.augmentation line 279
34. theorem OAI.NuclearUltrapower.Elementary.mem_augmentation line 284
35. theorem OAI.NuclearUltrapower.Elementary.augmentation_invariant line 287
36. def OAI.NuclearUltrapower.Elementary.augmentationVector line 292
37. theorem OAI.NuclearUltrapower.Elementary.augmentationVector_mem line 295
38. theorem OAI.NuclearUltrapower.Elementary.augmentationVector_ne_zero line 298
39. instance OAI.NuclearUltrapower.Elementary.augmentation_nontrivial line 307
40. def OAI.NuclearUltrapower.Elementary.augmentationRep line 314
41. theorem OAI.NuclearUltrapower.Elementary.augmentation_no_translation_invariants line 318

    Source documentation

    A translation-fixed vector in the augmentation representation is zero.

    theorem augmentation_no_translation_invariants (f : augmentationRep)
        (hf : ∀ v : IntegralVector3, augmentationRep.action (integralTranslation v) f = f) :
        f = 0 := by
    …

    Mentions: OAI.NuclearUltrapower.Elementary.augmentationRep, OAI.NuclearUltrapower.IntegralVector3, OAI.NuclearUltrapower.Elementary.integralTranslation

42. theorem OAI.NuclearUltrapower.Elementary.augmentation_pull_translation line 343

    Source documentation

    All positive dilation pullbacks kill the translation subgroup.

    theorem augmentation_pull_translation (j : ℕ) (hj : 0 < j) (v : IntegralVector3) :
        augmentationRep.action ((integralTheta ^ j) (integralTranslation v)) = 1 := by
    …

    Mentions: OAI.NuclearUltrapower.IntegralVector3, OAI.NuclearUltrapower.Elementary.integralTheta, OAI.NuclearUltrapower.Elementary.integralTranslation

43. theorem OAI.NuclearUltrapower.Elementary.exists_aperiodic_integral_rep line 359

    Source documentation

    The required irreducible mod-two representation is a constituent of the augmentation representation, hence has no translation-fixed vectors.

    theorem exists_aperiodic_integral_rep :
        ∃ π : FiniteUnitaryRep.{0,0} IntegralGroup, π.Irreducible ∧
          (∀ j : ℕ, 0 < j → ¬ π.Equivalent (π.pull (integralTheta ^ j))) := by
    …

    Mentions: OAI.NuclearUltrapower.Elementary.IntegralGroup, OAI.NuclearUltrapower.Elementary.integralTheta

44. theorem OAI.NuclearUltrapower.Elementary.transvection_one_mem line 394
45. def OAI.NuclearUltrapower.Elementary.transvectionHom line 398
46. theorem OAI.NuclearUltrapower.Elementary.transvection_mem line 403
47. def OAI.NuclearUltrapower.Elementary.elementaryTransvection line 414
48. def OAI.NuclearUltrapower.Elementary.basisVector line 417
49. theorem OAI.NuclearUltrapower.Elementary.transvection_basis line 419
50. def OAI.NuclearUltrapower.Elementary.linearInclusion line 424
51. theorem OAI.NuclearUltrapower.Elementary.conjugate_translation line 426
52. theorem OAI.NuclearUltrapower.Elementary.translation_add line 435
53. theorem OAI.NuclearUltrapower.Elementary.translation_neg line 439
54. theorem OAI.NuclearUltrapower.Elementary.translation_sub line 443
55. theorem OAI.NuclearUltrapower.Elementary.vector_decomp line 447
56. theorem OAI.NuclearUltrapower.Elementary.translation_zsmul line 451
57. theorem OAI.NuclearUltrapower.Elementary.translation_three line 455
58. theorem OAI.NuclearUltrapower.Elementary.normal_form line 465
59. def OAI.NuclearUltrapower.Displacement.dist line 480
60. theorem OAI.NuclearUltrapower.Displacement.mul_le line 482
61. theorem OAI.NuclearUltrapower.Displacement.inv line 493
62. theorem OAI.NuclearUltrapower.Displacement.prod_le line 502
63. theorem OAI.NuclearUltrapower.Displacement.conjugate line 510
64. theorem OAI.NuclearUltrapower.Displacement.change_vector line 523
65. theorem OAI.NuclearUltrapower.unitary_orbit_norm_le line 548

    Source documentation

    The closest point to zero in a closed convex unitary orbit hull is fixed. This supplies the bounded-orbit implication without using property T as an axiom.

    theorem unitary_orbit_norm_le (ρ : Γ →* (H ≃ₗᵢ[ℂ] H))
        (hno : ∀ y : H, (∀ g, ρ g y = y) → y = 0)
        (x : H) (r : ℝ) (hbound : ∀ g, ‖ρ g x - x‖ ≤ r) : ‖x‖ ≤ r := by
    …

66. def OAI.NuclearUltrapower.Elementary.kazhdanSet line 595

    Source documentation

    An explicit finite set in the honest integral elementary subgroup.

    def kazhdanSet : Finset IntegralGroup :=
    …

    Mentions: OAI.NuclearUltrapower.Elementary.IntegralGroup

67. theorem OAI.NuclearUltrapower.Elementary.kazhdanSet_nonempty line 598
68. theorem OAI.NuclearUltrapower.Elementary.kazhdanSet_generates line 603
69. theorem OAI.NuclearUltrapower.Elementary.translation_line_displacement line 631
70. theorem OAI.NuclearUltrapower.Elementary.translation_displacement line 651
71. theorem OAI.NuclearUltrapower.Elementary.integral_displacement line 668
72. theorem OAI.NuclearUltrapower.Elementary.kazhdan_energy line 681

    Source documentation

    This is the needed absolute gap, proved from the certified elementary gap and the elementary conjugacy identities on integral translations.

    theorem kazhdan_energy (ρ : IntegralGroup →* (H ≃ₗᵢ[ℂ] H))
        (hno : ∀ y : H, (∀ g, ρ g y = y) → y = 0) (x : H) :
        (1/4000 : ℝ) * ‖x‖ ^ 2 ≤ energy kazhdanSet ρ x := by
    …

    Mentions: OAI.NuclearUltrapower.Elementary.IntegralGroup, OAI.NuclearUltrapower.Elementary.kazhdanSet

73. theorem OAI.NuclearUltrapower.Elementary.hasKazhdanGap line 735