OAI/Geometry/HarmonicGrowth/Realization.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicCounterexample.laplace_congr line 14
  2. lemma OAI.HarmonicCounterexample.laplace_eq_euclidean_of_flat line 20
  3. lemma OAI.HarmonicCounterexample.Cartesian.synthesized_harmonic_at_ne_zero line 42
  4. abbrev OAI.HarmonicCounterexample.Angular.evaluate line 120
  5. lemma OAI.HarmonicCounterexample.Angular.evaluate_smooth line 122
  6. lemma OAI.HarmonicCounterexample.Angular.coordDeriv_evaluate line 129
  7. lemma OAI.HarmonicCounterexample.Angular.euler_evaluate line 151
  8. lemma OAI.HarmonicCounterexample.Angular.euclideanLaplacian_evaluate line 157
  9. lemma OAI.HarmonicCounterexample.Angular.harmonicPolynomials_euler line 162
  10. lemma OAI.HarmonicCounterexample.Angular.harmonicPolynomials_harmonic line 166
  11. lemma OAI.HarmonicCounterexample.Angular.evaluate_injective line 183
  12. lemma OAI.HarmonicCounterexample.Angular.evaluate_homogeneous line 189
  13. lemma OAI.HarmonicCounterexample.Angular.evaluate_zero_of_pos_degree line 204
  14. lemma OAI.HarmonicCounterexample.Angular.evaluate_sum line 208
  15. lemma OAI.HarmonicCounterexample.Angular.evaluate_smul line 211
  16. lemma OAI.HarmonicCounterexample.Angular.coordinate_radius_smul line 214
  17. lemma OAI.HarmonicCounterexample.Angular.hopf_evaluate line 230
  18. lemma OAI.HarmonicCounterexample.Angular.evaluate_zero_of_core line 253
  19. lemma OAI.HarmonicCounterexample.Angular.evaluate_eq_of_core line 279

    Source documentation

    Equality on the flat core determines the actual polynomial, not merely its restriction to a formal angular vector space.

    lemma evaluate_eq_of_core {P Q : PolynomialSpace n}
    (h : ∀ x, squareRadius x < 1 → evaluate P x = evaluate Q x) : P = Q := by
…

    Mentions: OAI.HarmonicCounterexample.Angular.PolynomialSpace, OAI.HarmonicCounterexample.Angular.evaluate

  20. lemma OAI.HarmonicCounterexample.Angular.rotation_evaluate line 286
  21. lemma OAI.HarmonicCounterexample.Cartesian.synthesized_core_eq line 303
  22. lemma OAI.HarmonicCounterexample.Cartesian.synthesized_harmonic_at_zero line 313
  23. lemma OAI.HarmonicCounterexample.Cartesian.synthesized_injective_from_core line 332

    Source documentation

    Global vanishing of synthesized functions forces vanishing of the initial polynomial. No limiting separation argument, ODE inverse, or unique-continuation claim is hidden here: the regular flow equals its polynomial on the open core.

    lemma synthesized_injective_from_core {l : ℝ} {P : ι → PolynomialSpace n}
    {Y : ℝ → ι → ℝ} {c : ι → ℝ}
    (hc : ∀ t ≤ 0, Y t = Real.exp (l*t) • c)
    (hz : synthesized l (fun i => evaluate (P i)) Y = 0) :
    ∑ i,c i • P i = 0 := by
…

    Mentions: OAI.HarmonicCounterexample.Cartesian.synthesized

  24. def OAI.HarmonicCounterexample.Angular.roundEigenvalue line 355

    Source documentation

    The round eigenvalue in degree l on S^(n-1).

    def roundEigenvalue (n l : ℕ) : ℝ := (l:ℝ)*((l:ℝ)+(n:ℝ)-2)
  25. lemma OAI.HarmonicCounterexample.Angular.roundEigenvalue_nonneg line 357
  26. def OAI.HarmonicCounterexample.Angular.angularOperator line 364

    Source documentation

    The actual negative Berger Laplacian on the genuine harmonic-polynomial space. Here c is the horizontal metric coefficient and q the squared Hopf stretch (the manuscript q).

    def angularOperator (J : ComplexStructure (Fin n)) (l : ℕ) (c q : ℝ) :
    harmonicPolynomials n l →L[ℝ] harmonicPolynomials n l :=
…

    Mentions: OAI.HarmonicCounterexample.Angular.harmonicPolynomials

  27. lemma OAI.HarmonicCounterexample.Angular.angularOperator_round line 369
  28. lemma OAI.HarmonicCounterexample.Angular.angularOperator_inner line 375
  29. lemma OAI.HarmonicCounterexample.Angular.angularOperator_symmetric line 382
  30. lemma OAI.HarmonicCounterexample.Angular.angularOperator_lower line 393
  31. lemma OAI.HarmonicCounterexample.Angular.angularOperator_nonnegative_of_one_le line 404
  32. lemma OAI.HarmonicCounterexample.Angular.angularOperator_positive_lower line 418
  33. lemma OAI.HarmonicCounterexample.Angular.angularOperator_nonnegative line 444
  34. lemma OAI.HarmonicCounterexample.Angular.angularOperator_norm_le line 451
  35. lemma OAI.HarmonicCounterexample.Angular.angularOperator_smooth line 468
  36. lemma OAI.HarmonicCounterexample.Angular.angularOperator_glued_smooth line 480

    Source documentation

    Switching the genuine angular rotation on an open round gap is smooth, although the label itself need not be continuous there.

    lemma angularOperator_glued_smooth (J : ℝ → ComplexStructure (Fin n)) (l : ℕ)
    {c q : ℝ → ℝ} (hc : ContDiff ℝ ∞ c) (hq : ContDiff ℝ ∞ q)
    (hc0 : ∀ t,c t ≠ 0) (hq0 : ∀ t,q t ≠ 0)
    (hJ : ∀ t,(∀ᶠ s in nhds t,J s = J t) ∨ (∀ᶠ s in nhds t,q s = 1)) :
    ContDiff ℝ ∞ (fun t => angularOperator (J t) l (c t) (q t)) := by
…

    Mentions: OAI.HarmonicCounterexample.Angular.angularOperator

  37. def OAI.HarmonicCounterexample.Angular.coordinates line 513

    Source documentation

    Coordinates in a fixed basis of actual harmonic polynomials.

    def coordinates (b : Basis ι ℝ (harmonicPolynomials n l)) :
    harmonicPolynomials n l ≃L[ℝ] (ι → ℝ) := b.equivFun.toContinuousLinearEquiv

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.Angular.harmonicPolynomials

  38. lemma OAI.HarmonicCounterexample.Angular.coordinates_sum line 516
  39. lemma OAI.HarmonicCounterexample.Angular.basis_evaluate line 519
  40. lemma OAI.HarmonicCounterexample.Angular.basis_operator_coordinates line 527
  41. lemma OAI.HarmonicCounterexample.Angular.square_rotation_basis_evaluate line 538
  42. lemma OAI.HarmonicCounterexample.Angular.angularOperator_basis_coordinates line 550
  43. structure OAI.HarmonicCounterexample.Construction.Stream line 578

    Source documentation

    A single constructed infinite history, including the thresholds and exact whole-period equalities, for any prescribed determinant-one simultaneous target.

    structure Stream (target:∀l:Fin L,Matrix.SpecialLinearGroup (Index l.val) ℝ) where
…

    Mentions: OAI.HarmonicCounterexample.Construction.L, OAI.HarmonicCounterexample.Construction.Index

  44. lemma OAI.HarmonicCounterexample.Construction.exists_stream line 602
  45. instance OAI.HarmonicCounterexample.Construction.Stream.(instance at line 626) line 626
  46. def OAI.HarmonicCounterexample.Construction.Stream.q line 628
  47. def OAI.HarmonicCounterexample.Construction.Stream.c line 629
  48. def OAI.HarmonicCounterexample.Construction.Stream.J line 630
  49. lemma OAI.HarmonicCounterexample.Construction.Stream.q_pos line 634
  50. lemma OAI.HarmonicCounterexample.Construction.Stream.q_smooth line 635
  51. lemma OAI.HarmonicCounterexample.Construction.Stream.c_pos line 636
  52. lemma OAI.HarmonicCounterexample.Construction.Stream.c_smooth line 637
  53. lemma OAI.HarmonicCounterexample.Construction.Stream.J_local line 638
  54. lemma OAI.HarmonicCounterexample.Construction.Stream.q_center line 642
  55. lemma OAI.HarmonicCounterexample.Construction.Stream.c_center line 643
  56. def OAI.HarmonicCounterexample.Construction.Stream.metric line 645
  57. lemma OAI.HarmonicCounterexample.Construction.Stream.geometry_main line 648
  58. lemma OAI.HarmonicCounterexample.Construction.Stream.ricci line 653
  59. lemma OAI.HarmonicCounterexample.Construction.Stream.drift_eq line 664
  60. lemma OAI.HarmonicCounterexample.Construction.Stream.coefficient_eq line 667