OAI/Geometry/HarmonicGrowth/HopfSpectrum.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HarmonicCounterexample.Certificate.mean_root_lt line 14

    Source documentation

    Convexity of d(d+h), proved by the exact nonnegative-square identity. This is used to certify a strict mean-exponent bound from rational eigenvalues.

    theorem mean_root_lt {ι : Type*} (s : Finset ι) (w d : ι → ℝ)
    (h k : ℝ) (hw : ∀ i ∈ s,0 ≤ w i) (hkh : 0 < 2*k+h)
    (hspec : (∑ i ∈ s,w i*(d i*(d i+h))) < k*(k+h)*∑ i ∈ s,w i) :
    (∑ i ∈ s,w i*d i) < k*∑ i ∈ s,w i := by
…
  2. def OAI.HarmonicCounterexample.Certificate.eigenvalue line 33

    Source documentation

    The source eigenvalue, with its exact pinned normalization.

    def eigenvalue (l b : ℕ) : ℝ :=
…

    Mentions: OAI.HarmonicCounterexample.b

  3. def OAI.HarmonicCounterexample.Certificate.exponent line 36
  4. lemma OAI.HarmonicCounterexample.Certificate.eigenvalue_pos line 38
  5. lemma OAI.HarmonicCounterexample.Certificate.exponent_equation line 49
  6. lemma OAI.HarmonicCounterexample.Certificate.exponent_pos line 56
  7. def OAI.HarmonicCounterexample.Certificate.pairMultiplicity line 65

    Source documentation

    A paired charge count, as a rational integer-valued polynomial.

    def pairMultiplicity (l b : ℕ) : ℚ :=
…

    Mentions: OAI.HarmonicCounterexample.b

  8. lemma OAI.HarmonicCounterexample.Certificate.pairMultiplicity_pos line 68
  9. lemma OAI.HarmonicCounterexample.Certificate.pairMultiplicity_sum line 79
  10. lemma OAI.HarmonicCounterexample.Certificate.pairMultiplicity_charge_sum line 85
  11. def OAI.HarmonicCounterexample.Certificate.hopfMultiplicity line 106

    Source documentation

    The exact source Hopf multiplicity, obtained as the bihomogeneous kernel minus its Laplacian target, not an asymptotic density.

    def hopfMultiplicity (a b : ℕ) : ℕ :=
…

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.b

  12. lemma OAI.HarmonicCounterexample.Certificate.binomRat_seven_from_six line 109
  13. lemma OAI.HarmonicCounterexample.Certificate.hopfMultiplicity_rat line 115
  14. lemma OAI.HarmonicCounterexample.Certificate.pairMultiplicity_eq line 128
  15. lemma OAI.HarmonicCounterexample.Certificate.hopfMultiplicity_symm line 135
  16. lemma OAI.HarmonicCounterexample.Construction.d0_bounds line 150
  17. lemma OAI.HarmonicCounterexample.Construction.d0_sum line 159
  18. def OAI.HarmonicCounterexample.Construction.lambda line 166
  19. def OAI.HarmonicCounterexample.Construction.root line 168
  20. lemma OAI.HarmonicCounterexample.Construction.lambda_exact line 170
  21. lemma OAI.HarmonicCounterexample.Construction.lambda_pos line 178
  22. lemma OAI.HarmonicCounterexample.Construction.root_pos line 185
  23. lemma OAI.HarmonicCounterexample.Construction.root_eq line 189
  24. lemma OAI.HarmonicCounterexample.Construction.lambda_of_charge line 193
  25. lemma OAI.HarmonicCounterexample.Construction.mean_root_from_lambda line 200
  26. lemma OAI.HarmonicCounterexample.Construction.full_mean_root line 207
  27. def OAI.HarmonicCounterexample.ComplexAngular.biWeight line 234
  28. def OAI.HarmonicCounterexample.ComplexAngular.biSpace line 236
  29. lemma OAI.HarmonicCounterexample.ComplexAngular.biWeight_apply line 240
  30. abbrev OAI.HarmonicCounterexample.ComplexAngular.DegreeIndex line 249
  31. lemma OAI.HarmonicCounterexample.ComplexAngular.degreeIndex_mem line 252
  32. def OAI.HarmonicCounterexample.ComplexAngular.biIndexEquiv line 258

    Source documentation

    The actual monomials of bidegree (p,q) are independently chosen left and right multisets. This is an equivalence, not an assumed multiplicity.

    def biIndexEquiv (p q : ℕ) :
    {d : (ι ⊕ ι) →₀ ℕ | weight biWeight d = (p,q)} ≃
      DegreeIndex ι p × DegreeIndex ι q where
…

    Mentions: OAI.HarmonicCounterexample.ComplexAngular.biWeight, OAI.HarmonicCounterexample.ComplexAngular.DegreeIndex

  33. instance OAI.HarmonicCounterexample.ComplexAngular.biIndex_fintype line 278
  34. lemma OAI.HarmonicCounterexample.ComplexAngular.biSpace_finrank line 282
  35. instance OAI.HarmonicCounterexample.ComplexAngular.biSpace_finite line 294
  36. lemma OAI.HarmonicCounterexample.ComplexAngular.conjugate_mem_biSpace line 312
  37. lemma OAI.HarmonicCounterexample.ComplexAngular.quadric_bihomogeneous line 320
  38. def OAI.HarmonicCounterexample.ComplexAngular.biQuadricMultiply line 326
  39. lemma OAI.HarmonicCounterexample.ComplexAngular.biQuadricMultiply_injective line 335
  40. def OAI.HarmonicCounterexample.ComplexAngular.biLaplacian line 341
  41. lemma OAI.HarmonicCounterexample.ComplexAngular.biLaplacian_surjective line 352
  42. def OAI.HarmonicCounterexample.ComplexAngular.biHarmonic line 369

    Source documentation

    Actual bihomogeneous harmonic polynomials.

    def biHarmonic (p q : ℕ) : Submodule ℂ (SplitPolynomial ι) :=
…

    Mentions: OAI.HarmonicCounterexample.ComplexAngular.SplitPolynomial

  43. instance OAI.HarmonicCounterexample.ComplexAngular.biHarmonic_finite line 372
  44. def OAI.HarmonicCounterexample.ComplexAngular.biKernelEquiv line 375
  45. lemma OAI.HarmonicCounterexample.ComplexAngular.biHarmonic_finrank_add line 384
  46. lemma OAI.HarmonicCounterexample.ComplexAngular.biSpace_left_weight line 407
  47. lemma OAI.HarmonicCounterexample.ComplexAngular.biSpace_right_weight line 416
  48. lemma OAI.HarmonicCounterexample.ComplexAngular.biSpace_leftEuler line 425
  49. lemma OAI.HarmonicCounterexample.ComplexAngular.biSpace_rightEuler line 433
  50. lemma OAI.HarmonicCounterexample.Control.splitMatrix_block line 453
  51. lemma OAI.HarmonicCounterexample.Control.hopf_charge line 462

    Source documentation

    The true Hopf vector field on actual bihomogeneous polynomials has its literal integer charge p-q; it is not postulated as a spectral label.

    lemma hopf_charge {s p q : ℕ} {P : SplitPolynomial (Fin s)}
    (hP : P ∈ biSpace p q) :
    linearField (splitMatrix (ComplexStructure.block s)) P=
      (Complex.I*((p:ℂ)-(q:ℂ))) • P := by
…

    Mentions: OAI.HarmonicCounterexample.Control.linearField

  52. lemma OAI.HarmonicCounterexample.Control.hopf_square_eigenvalue line 475

    Source documentation

    The actual nonnegative Hopf-square eigenvalue entering the Berger angular operator, including charge zero and both signs of p-q.

    lemma hopf_square_eigenvalue {s p q : ℕ} {P : SplitPolynomial (Fin s)}
    (hP : P ∈ biSpace p q) :
    -linearField (splitMatrix (ComplexStructure.block s))
      (linearField (splitMatrix (ComplexStructure.block s)) P)=
      (((p:ℂ)-(q:ℂ))^2) • P := by
…

    Mentions: OAI.HarmonicCounterexample.Control.linearField

  53. lemma OAI.HarmonicCounterexample.RealForm.realPart_map line 499
  54. lemma OAI.HarmonicCounterexample.RealForm.eigen_realPart_zero line 505
  55. lemma OAI.HarmonicCounterexample.RealForm.eigen_square_realPart line 516
  56. lemma OAI.HarmonicCounterexample.ComplexAngular.biSpace_homogeneous line 538
  57. def OAI.HarmonicCounterexample.ComplexAngular.biHarmonicInclusion line 548
  58. lemma OAI.HarmonicCounterexample.ComplexAngular.biHarmonicInclusion_injective line 553
  59. def OAI.HarmonicCounterexample.Control.biRealCartesian line 568
  60. lemma OAI.HarmonicCounterexample.Control.biHarmonic_charge line 573
  61. lemma OAI.HarmonicCounterexample.Control.biRealCartesian_injective line 583
  62. lemma OAI.HarmonicCounterexample.Control.biRealCartesian_square line 595
  63. lemma OAI.HarmonicCounterexample.ComplexAngular.pderiv_left_zero line 620
  64. lemma OAI.HarmonicCounterexample.ComplexAngular.pderiv_right_zero line 631
  65. lemma OAI.HarmonicCounterexample.ComplexAngular.biHarmonic_zero_right line 642
  66. lemma OAI.HarmonicCounterexample.ComplexAngular.biHarmonic_zero_left line 648
  67. lemma OAI.HarmonicCounterexample.ComplexAngular.biHarmonic_finrank line 671

    Source documentation

    Exact dimension formula including the holomorphic and antiholomorphic boundary spaces. The subtracted term is absent there, as in the manuscript.

    lemma biHarmonic_finrank [Nontrivial ι] (p q : ℕ) :
    Module.finrank ℂ (biHarmonic (ι := ι) p q) =
…

    Mentions: OAI.HarmonicCounterexample.ComplexAngular.biHarmonic

  68. lemma OAI.HarmonicCounterexample.eigen_dimension_lower line 703
  69. lemma OAI.HarmonicCounterexample.Construction.biharmonic_dimension line 721
  70. lemma OAI.HarmonicCounterexample.Construction.biharmonic_real_dimension line 741
  71. lemma OAI.HarmonicCounterexample.Construction.d0_card line 745
  72. lemma OAI.HarmonicCounterexample.Construction.bi_eigenspace_dimension line 751
  73. lemma OAI.HarmonicCounterexample.Construction.eigen_multiplicity line 764