OAI/Analysis/PlaneSpectrum/Basic.lean

GitHub source file

112 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PlaneFiveColor.Spectral.E line 9
  2. def OAI.PlaneFiveColor.Spectral.K line 11
  3. theorem OAI.PlaneFiveColor.Spectral.K_pow_surjective line 17
  4. instance OAI.PlaneFiveColor.Spectral.K_rootable line 32
  5. theorem OAI.PlaneFiveColor.Spectral.finite_image_trivial line 35

    Source documentation

    The group-theoretic step behind the zero-mass coset argument.

    theorem finite_image_trivial {G H : Type*} [Group G] [Group H] [Finite H]
    [RootableBy G ℕ] (f : G →* H) (g : G) : f g = 1 := by
…
  6. def OAI.PlaneFiveColor.Spectral.DiscreteE line 44

    Source documentation

    A separate synonym ensures that the dual uses the discrete topology, not the Euclidean topology inherited by the embedded algebraic field.

    def DiscreteE := Multiplicative E deriving CommGroup

    Mentions: OAI.PlaneFiveColor.Spectral.E

  7. instance OAI.PlaneFiveColor.Spectral.(instance at line 45) line 45
  8. instance OAI.PlaneFiveColor.Spectral.(instance at line 46) line 46
  9. instance OAI.PlaneFiveColor.Spectral.(instance at line 47) line 47
  10. abbrev OAI.PlaneFiveColor.Spectral.D line 48
  11. example OAI.PlaneFiveColor.Spectral.(example at line 50) line 50
  12. example OAI.PlaneFiveColor.Spectral.(example at line 51) line 51
  13. instance OAI.PlaneFiveColor.Spectral.E_countable line 53
  14. instance OAI.PlaneFiveColor.Spectral.(instance at line 60) line 60
  15. instance OAI.PlaneFiveColor.Spectral.(instance at line 62) line 62
  16. def OAI.PlaneFiveColor.Spectral.embed line 67

    Source documentation

    The inclusion into the usual complex plane, with no continuity assertion needed on its discrete domain.

    def embed (z : DiscreteE) : ℂ := ((Multiplicative.toAdd z : E) : ℂ)

    Mentions: OAI.PlaneFiveColor.Spectral.DiscreteE, OAI.PlaneFiveColor.Spectral.E

  17. theorem OAI.PlaneFiveColor.Spectral.embed_one line 69
  18. theorem OAI.PlaneFiveColor.Spectral.embed_mul line 70
  19. def OAI.PlaneFiveColor.Spectral.j line 73

    Source documentation

    The manuscript's ordinary character parametrization.

    def j (ξ : ℂ) : D where
…

    Mentions: OAI.PlaneFiveColor.Spectral.D

  20. theorem OAI.PlaneFiveColor.Spectral.j_apply line 79
  21. theorem OAI.PlaneFiveColor.Spectral.j_zero line 82
  22. theorem OAI.PlaneFiveColor.Spectral.j_add line 87
  23. def OAI.PlaneFiveColor.Spectral.jHom line 94
  24. def OAI.PlaneFiveColor.Spectral.C line 100

    Source documentation

    The subgroup C is not replaced by its closure.

    def C : Subgroup D := jHom.range

    Mentions: OAI.PlaneFiveColor.Spectral.D

  25. theorem OAI.PlaneFiveColor.Spectral.continuous_j line 102
  26. theorem OAI.PlaneFiveColor.Spectral.fixed_of_finite_orbit line 109

    Source documentation

    A divisible group cannot act nontrivially on a finite orbit.

    theorem fixed_of_finite_orbit {G X : Type*} [Group G] [MulAction G X]
    [RootableBy G ℕ] (x : X) (hf : (MulAction.orbit G x).Finite) (g : G) :
    g • x = x := by
…
  27. instance OAI.PlaneFiveColor.Spectral.(instance at line 118) line 118
  28. instance OAI.PlaneFiveColor.Spectral.(instance at line 119) line 119
  29. theorem OAI.PlaneFiveColor.Spectral.measurableSet_C line 121
  30. def OAI.PlaneFiveColor.Spectral.scaleE line 128

    Source documentation

    Multiplication of the argument of a character.

    def scaleE (a : E) : DiscreteE →ₜ* DiscreteE where
…

    Mentions: OAI.PlaneFiveColor.Spectral.E, OAI.PlaneFiveColor.Spectral.DiscreteE

  31. def OAI.PlaneFiveColor.Spectral.scalar line 137
  32. theorem OAI.PlaneFiveColor.Spectral.scalar_apply line 139
  33. theorem OAI.PlaneFiveColor.Spectral.scalar_one line 142
  34. theorem OAI.PlaneFiveColor.Spectral.scalar_mul line 149
  35. theorem OAI.PlaneFiveColor.Spectral.scalar_add line 157
  36. theorem OAI.PlaneFiveColor.Spectral.scalar_j line 165
  37. theorem OAI.PlaneFiveColor.Spectral.scalar_mem_C line 176
  38. theorem OAI.PlaneFiveColor.Spectral.scalar_mem_C_iff line 180
  39. theorem OAI.PlaneFiveColor.Spectral.fixed_of_positive_fiber line 189

    Source documentation

    Positive fibers of an equivariant partition have finite orbit. This uses only finite measure and measurability of the fibers, not a measurable quotient.

    theorem fixed_of_positive_fiber {G X Y : Type*} [Group G] [RootableBy G ℕ]
    [MulAction G X] [MulAction G Y] [MeasurableSpace X]
    (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ]
    (π : X → Y) (heq : ∀ (g : G) (x : X), π (g • x) = g • π x)
    (hmeas : ∀ y, MeasurableSet (π ⁻¹' {y}))
    (hinv : ∀ g : G, MeasureTheory.MeasurePreserving (fun x : X => g • x) μ μ)
    (y : Y) (hpos : 0 < μ (π ⁻¹' {y})) (g : G) : g • y = y := by
…
  40. def OAI.PlaneFiveColor.Spectral.kCoeff line 224
  41. theorem OAI.PlaneFiveColor.Spectral.kCoeff_one line 226
  42. theorem OAI.PlaneFiveColor.Spectral.kCoeff_mul line 227
  43. def OAI.PlaneFiveColor.Spectral.scalarHom line 229
  44. instance OAI.PlaneFiveColor.Spectral.(instance at line 234) line 234
  45. abbrev OAI.PlaneFiveColor.Spectral.Cosets line 239
  46. def OAI.PlaneFiveColor.Spectral.cosetScalar line 241
  47. instance OAI.PlaneFiveColor.Spectral.(instance at line 244) line 244
  48. theorem OAI.PlaneFiveColor.Spectral.quotient_equivariant line 258
  49. theorem OAI.PlaneFiveColor.Spectral.measurableSet_coset line 261
  50. theorem OAI.PlaneFiveColor.Spectral.scalar_neg line 272
  51. theorem OAI.PlaneFiveColor.Spectral.scalar_sub line 280
  52. def OAI.PlaneFiveColor.Spectral.minusOne line 284
  53. theorem OAI.PlaneFiveColor.Spectral.kCoeff_minusOne line 288
  54. theorem OAI.PlaneFiveColor.Spectral.coset_fixed_minusOne line 290
  55. def OAI.PlaneFiveColor.Spectral.IsWild line 300

    Source documentation

    The source's wild-law condition; probability is provided as a measure instance.

    def IsWild (ν : MeasureTheory.Measure D) : Prop :=
…

    Mentions: OAI.PlaneFiveColor.Spectral.D

  56. theorem OAI.PlaneFiveColor.Spectral.wild_coset_null line 304
  57. theorem OAI.PlaneFiveColor.Spectral.wild_div_mem_null line 319
  58. theorem OAI.PlaneFiveColor.Spectral.wild_independent_difference line 326
  59. theorem OAI.PlaneFiveColor.Spectral.continuous_scalar line 337
  60. theorem OAI.PlaneFiveColor.Spectral.frequency_zero_of_rational_tests line 341

    Source documentation

    Rational tests identify the frequency of a real continuous character.

    theorem frequency_zero_of_rational_tests (a : ℝ)
    (h : ∀ q : ℚ, Circle.exp (a * (q : ℝ)) = 1) : a = 0 := by
…
  61. def OAI.PlaneFiveColor.Spectral.imagUnit line 358
  62. theorem OAI.PlaneFiveColor.Spectral.coe_imagUnit line 363
  63. theorem OAI.PlaneFiveColor.Spectral.j_eq_one_iff line 365
  64. theorem OAI.PlaneFiveColor.Spectral.j_neg line 382
  65. theorem OAI.PlaneFiveColor.Spectral.j_sub line 385
  66. theorem OAI.PlaneFiveColor.Spectral.j_injective line 388
  67. theorem OAI.PlaneFiveColor.Spectral.j_measurableEmbedding line 394
  68. theorem OAI.PlaneFiveColor.Spectral.algebraic_complex_iff_coordinates line 399

    Source documentation

    The complex algebraic closure used above is precisely F(i) from the source, not a different countable plane.

    theorem algebraic_complex_iff_coordinates (z : ℂ) :
    IsAlgebraic ℚ z ↔ IsAlgebraic ℚ z.re ∧ IsAlgebraic ℚ z.im := by
…
  69. theorem OAI.PlaneFiveColor.Spectral.real_character line 424

    Source documentation

    Ordinary one-dimensional characters, proved from the covering property of exp.

    theorem real_character (f : ℝ → Circle) (hf : Continuous f)
    (hmul : ∀ x y, f (x + y) = f x * f y) :
    ∃ a : ℝ, ∀ t, f t = Circle.exp (a * t) := by
…
  70. abbrev OAI.PlaneFiveColor.Spectral.F line 452
  71. theorem OAI.PlaneFiveColor.Spectral.dense_F line 454
  72. theorem OAI.PlaneFiveColor.Spectral.algebraic_real_character line 460

    Source documentation

    The source's exact ordinary-character description on the dense real algebraic field.

    theorem algebraic_real_character (f : F → Circle) (hf : Continuous f)
    (hmul : ∀ x y, f (x + y) = f x * f y) :
    ∃ a : ℝ, ∀ t : F, f t = Circle.exp (a * (t : ℝ)) := by
…

    Mentions: OAI.PlaneFiveColor.Spectral.F

  73. def OAI.PlaneFiveColor.Spectral.ofF line 488

    Source documentation

    The real-algebraic inclusion into the algebraic plane.

    def ofF : F →+* E where
…

    Mentions: OAI.PlaneFiveColor.Spectral.F, OAI.PlaneFiveColor.Spectral.E

  74. theorem OAI.PlaneFiveColor.Spectral.coe_ofF line 496
  75. def OAI.PlaneFiveColor.Spectral.DiscreteF line 498
  76. instance OAI.PlaneFiveColor.Spectral.(instance at line 499) line 499
  77. instance OAI.PlaneFiveColor.Spectral.(instance at line 500) line 500
  78. instance OAI.PlaneFiveColor.Spectral.(instance at line 501) line 501
  79. abbrev OAI.PlaneFiveColor.Spectral.DF line 502
  80. instance OAI.PlaneFiveColor.Spectral.(instance at line 503) line 503
  81. instance OAI.PlaneFiveColor.Spectral.(instance at line 504) line 504
  82. def OAI.PlaneFiveColor.Spectral.embedF line 506
  83. theorem OAI.PlaneFiveColor.Spectral.embedF_one line 507
  84. theorem OAI.PlaneFiveColor.Spectral.embedF_mul line 508
  85. def OAI.PlaneFiveColor.Spectral.jF line 511

    Source documentation

    Standard frequencies for the real algebraic line; again use the actual image.

    def jF (l : ℝ) : DF where
…

    Mentions: OAI.PlaneFiveColor.Spectral.DF

  86. theorem OAI.PlaneFiveColor.Spectral.jF_apply line 517
  87. def OAI.PlaneFiveColor.Spectral.CF line 520
  88. theorem OAI.PlaneFiveColor.Spectral.continuous_jF line 522
  89. theorem OAI.PlaneFiveColor.Spectral.measurableSet_CF line 528
  90. def OAI.PlaneFiveColor.Spectral.lineHom line 535

    Source documentation

    The dual restriction to the line aF.

    def lineHom (a : E) : DiscreteF →ₜ* DiscreteE where
…

    Mentions: OAI.PlaneFiveColor.Spectral.E, OAI.PlaneFiveColor.Spectral.DiscreteF, OAI.PlaneFiveColor.Spectral.DiscreteE

  91. def OAI.PlaneFiveColor.Spectral.restrictLine line 544
  92. theorem OAI.PlaneFiveColor.Spectral.continuous_restrictLine line 546
  93. def OAI.PlaneFiveColor.Spectral.L line 549
  94. theorem OAI.PlaneFiveColor.Spectral.mem_L_iff line 552
  95. theorem OAI.PlaneFiveColor.Spectral.measurableSet_L line 571
  96. def OAI.PlaneFiveColor.Spectral.reF line 576
  97. def OAI.PlaneFiveColor.Spectral.imF line 578
  98. theorem OAI.PlaneFiveColor.Spectral.coe_reF line 581
  99. theorem OAI.PlaneFiveColor.Spectral.coe_imF line 582
  100. theorem OAI.PlaneFiveColor.Spectral.reF_add_imF line 584
  101. theorem OAI.PlaneFiveColor.Spectral.line_add line 589
  102. theorem OAI.PlaneFiveColor.Spectral.line_mul_real line 598
  103. theorem OAI.PlaneFiveColor.Spectral.line_sub line 605
  104. theorem OAI.PlaneFiveColor.Spectral.orthogonal_lines line 610
  105. theorem OAI.PlaneFiveColor.Spectral.line_one_and_nonreal line 635

    Source documentation

    Two genuinely independent algebraic directions force an ordinary character.

    theorem line_one_and_nonreal {d : D} (h1 : d ∈ L 1) {w : E}
    (hw : d ∈ L w) (hn : imF w ≠ 0) : d ∈ C := by
…

    Mentions: OAI.PlaneFiveColor.Spectral.D, OAI.PlaneFiveColor.Spectral.L, OAI.PlaneFiveColor.Spectral.E, OAI.PlaneFiveColor.Spectral.imF, OAI.PlaneFiveColor.Spectral.C

  106. theorem OAI.PlaneFiveColor.Spectral.scalar_line line 651
  107. theorem OAI.PlaneFiveColor.Spectral.independent_lines line 656
  108. theorem OAI.PlaneFiveColor.Spectral.kCoeff_inv line 662
  109. theorem OAI.PlaneFiveColor.Spectral.kCoeff_ne_zero line 667
  110. theorem OAI.PlaneFiveColor.Spectral.real_rotation_square line 672
  111. theorem OAI.PlaneFiveColor.Spectral.rotated_directions_independent line 684

    Source documentation

    Squared rotations index the distinct unoriented algebraic lines.

    theorem rotated_directions_independent {a : E} (ha : a ≠ 0) {u v : K}
    (huv : u ^ 2 ≠ v ^ 2) : imF ((a * kCoeff u)⁻¹ * (a * kCoeff v)) ≠ 0 := by
…

    Mentions: OAI.PlaneFiveColor.Spectral.E, OAI.PlaneFiveColor.Spectral.K, OAI.PlaneFiveColor.Spectral.imF, OAI.PlaneFiveColor.Spectral.kCoeff

  112. theorem OAI.PlaneFiveColor.Spectral.wild_line_null line 696

    Source documentation

    Complete line-event conclusion of the source's null-events lemma.

    theorem wild_line_null (ν : MeasureTheory.Measure D) [MeasureTheory.IsProbabilityMeasure ν]
    (hν : IsWild ν) {a : E} (ha : a ≠ 0) : ν (L a) = 0 := by
…

    Mentions: OAI.PlaneFiveColor.Spectral.D, OAI.PlaneFiveColor.Spectral.IsWild, OAI.PlaneFiveColor.Spectral.E, OAI.PlaneFiveColor.Spectral.L