OAI/Geometry/HarmonicGrowth/Berger.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicCounterexample.Berger.dot_self_nonneg line 15
  2. lemma OAI.HarmonicCounterexample.Berger.dot_self_pos line 18
  3. lemma OAI.HarmonicCounterexample.Berger.two_vector_bessel line 22

    Source documentation

    Bessel's two-vector inequality, without an implicit Euclidean norm instance.

    lemma two_vector_bessel {u v : ι → ℝ}
    (hu : u ⬝ᵥ u = 1) (hv : v ⬝ᵥ v = 1) (huv : u ⬝ᵥ v = 0)
    (w : ι → ℝ) : (u ⬝ᵥ w)^2 + (v ⬝ᵥ w)^2 ≤ w ⬝ᵥ w := by
…
  4. def OAI.HarmonicCounterexample.Berger.tensor line 37

    Source documentation

    Cartesian coefficient tensor of dr²+r²G(a,q,J), with u=x/r, v=Jx/r and c=a²q^(-1/m). The radial eigenvalue remains exactly one.

    def tensor (u v : ι → ℝ) (c q : ℝ) : Matrix ι ι ℝ :=
…
  5. lemma OAI.HarmonicCounterexample.Berger.tensor_symmetric line 41
  6. lemma OAI.HarmonicCounterexample.Berger.tensor_quadratic line 52
  7. theorem OAI.HarmonicCounterexample.Berger.tensor_lower_bound line 62

    Source documentation

    Uniform ellipticity with the exact three eigenvalue bounds.

    theorem tensor_lower_bound {u v : ι → ℝ}
    (hu : u ⬝ᵥ u = 1) (hv : v ⬝ᵥ v = 1) (huv : u ⬝ᵥ v = 0)
    {c q ell : ℝ} (hell1 : ell ≤ 1) (hellc : ell ≤ c) (hellcq : ell ≤ c*q)
    (w : ι → ℝ) : ell * (w ⬝ᵥ w) ≤ w ⬝ᵥ (tensor u v c q *ᵥ w) := by
…

    Mentions: OAI.HarmonicCounterexample.Berger.tensor

  8. theorem OAI.HarmonicCounterexample.Berger.tensor_posDef line 76

    Source documentation

    Actual positive definiteness of the Berger radial extension, including q<1 on the negative-amplitude control pulses.

    theorem tensor_posDef {u v : ι → ℝ}
    (hu : u ⬝ᵥ u = 1) (hv : v ⬝ᵥ v = 1) (huv : u ⬝ᵥ v = 0)
    {c q : ℝ} (hc : 0 < c) (hq : 0 < q) : (tensor u v c q).PosDef := by
…

    Mentions: OAI.HarmonicCounterexample.Berger.tensor

  9. lemma OAI.HarmonicCounterexample.Berger.tensor_radial line 89
  10. lemma OAI.HarmonicCounterexample.Berger.tensor_hopf line 99
  11. lemma OAI.HarmonicCounterexample.Berger.tensor_horizontal line 109
  12. structure OAI.HarmonicCounterexample.Berger.ComplexStructure line 131

    Source documentation

    Exactly the two standing equations for an orthogonal complex structure. Both orientation classes are permitted.

    structure ComplexStructure (ι : Type*) [Fintype ι] [DecidableEq ι] where
…
  13. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.skew line 139
  14. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.preserves_dot line 145
  15. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.orthogonal_radial line 152
  16. def OAI.HarmonicCounterexample.Berger.ComplexStructure.reindex line 163

    Source documentation

    Reindexing does not change either defining equation.

    def reindex {κ : Type*} [Fintype κ] [DecidableEq κ]
    (J : ComplexStructure ι) (e : κ ≃ ι) : ComplexStructure κ where
…

    Mentions: OAI.HarmonicCounterexample.Berger.ComplexStructure

  17. def OAI.HarmonicCounterexample.Berger.ComplexStructure.block line 174

    Source documentation

    A genuine model in every even dimension, not a nonemptiness assumption.

    def block (s : ℕ) : ComplexStructure (Fin s ⊕ Fin s) where
…

    Mentions: OAI.HarmonicCounterexample.Berger.ComplexStructure

  18. def OAI.HarmonicCounterexample.Berger.ComplexStructure.standard line 187
  19. abbrev OAI.HarmonicCounterexample.Cartesian.Coord line 207
  20. def OAI.HarmonicCounterexample.Cartesian.squareRadius line 209
  21. def OAI.HarmonicCounterexample.Cartesian.radius line 211
  22. def OAI.HarmonicCounterexample.Cartesian.logRadius line 213
  23. lemma OAI.HarmonicCounterexample.Cartesian.squareRadius_nonneg line 215
  24. lemma OAI.HarmonicCounterexample.Cartesian.squareRadius_zero line 219
  25. lemma OAI.HarmonicCounterexample.Cartesian.squareRadius_eq_zero line 222
  26. lemma OAI.HarmonicCounterexample.Cartesian.squareRadius_pos line 225
  27. lemma OAI.HarmonicCounterexample.Cartesian.radius_nonneg line 228
  28. lemma OAI.HarmonicCounterexample.Cartesian.radius_zero line 230
  29. lemma OAI.HarmonicCounterexample.Cartesian.radius_pos line 232
  30. lemma OAI.HarmonicCounterexample.Cartesian.radius_sq line 235
  31. lemma OAI.HarmonicCounterexample.Cartesian.squareRadius_smooth line 238
  32. lemma OAI.HarmonicCounterexample.Cartesian.radius_continuous line 242
  33. lemma OAI.HarmonicCounterexample.Cartesian.radius_smoothAt line 245
  34. lemma OAI.HarmonicCounterexample.Cartesian.logRadius_smoothAt line 248
  35. lemma OAI.HarmonicCounterexample.Cartesian.norm_le_radius line 252
  36. lemma OAI.HarmonicCounterexample.Cartesian.radius_sublevel_compact line 263

    Source documentation

    Euclidean radial sublevels are genuinely compact in the Cartesian space.

    lemma radius_sublevel_compact {n : ℕ} (R : ℝ) : IsCompact {x : Coord n | radius x ≤ R} := by
…

    Mentions: OAI.HarmonicCounterexample.Cartesian.Coord, OAI.HarmonicCounterexample.Cartesian.radius

  37. lemma OAI.HarmonicCounterexample.Cartesian.logRadius_eq_log_radius line 270
  38. lemma OAI.HarmonicCounterexample.Cartesian.exp_logRadius line 276
  39. lemma OAI.HarmonicCounterexample.Cartesian.radius_exp_bound line 280
  40. def OAI.HarmonicCounterexample.Cartesian.radialUnit line 302

    Source documentation

    Unit radial vector in the background Cartesian metric.

    def radialUnit {n : ℕ} (x : Coord n) : Coord n := (radius x)⁻¹ • x

    Mentions: OAI.HarmonicCounterexample.Cartesian.Coord, OAI.HarmonicCounterexample.Cartesian.radius

  41. def OAI.HarmonicCounterexample.Cartesian.hopfUnit line 305

    Source documentation

    Unit Hopf vector for the indicated orthogonal complex structure.

    def hopfUnit {n : ℕ} (J : ComplexStructure (Fin n)) (x : Coord n) : Coord n :=
…

    Mentions: OAI.HarmonicCounterexample.Cartesian.Coord

  42. lemma OAI.HarmonicCounterexample.Cartesian.radialUnit_unit line 308
  43. lemma OAI.HarmonicCounterexample.Cartesian.hopfUnit_unit line 316
  44. lemma OAI.HarmonicCounterexample.Cartesian.radial_hopf_orthogonal line 324
  45. lemma OAI.HarmonicCounterexample.Cartesian.radialUnit_smoothAt line 328
  46. lemma OAI.HarmonicCounterexample.Cartesian.hopfUnit_smoothAt line 332
  47. def OAI.HarmonicCounterexample.Cartesian.rawCoefficient line 342

    Source documentation

    The actual punctured Cartesian tensor; J may switch on round gaps.

    def rawCoefficient {n : ℕ} (c q : ℝ → ℝ) (J : ℝ → ComplexStructure (Fin n))
    (x : Coord n) : Matrix (Fin n) (Fin n) ℝ :=
…

    Mentions: OAI.HarmonicCounterexample.Cartesian.Coord

  48. lemma OAI.HarmonicCounterexample.Cartesian.rawCoefficient_posDef line 347
  49. lemma OAI.HarmonicCounterexample.Cartesian.fixedTensor_smoothAt line 357
  50. lemma OAI.HarmonicCounterexample.Cartesian.rawCoefficient_smoothAt_nonzero line 371
  51. lemma OAI.HarmonicCounterexample.Cartesian.rawCoefficient_euclidean line 388
  52. lemma OAI.HarmonicCounterexample.Cartesian.rawCoefficient_smooth line 398
  53. def OAI.HarmonicCounterexample.Cartesian.bergerMetric line 436

    Source documentation

    A concrete smooth metric from the manuscript's logarithmic Berger data. The local constancy alternative encodes switching J only inside round gaps.

    def bergerMetric {n : ℕ} (c q : ℝ → ℝ) (J : ℝ → ComplexStructure (Fin n))
    (hc : ContDiff ℝ ∞ c) (hq : ContDiff ℝ ∞ q)
    (hcp : ∀ t, 0 < c t) (hqp : ∀ t, 0 < q t)
    (hJ : ∀ t, (∀ᶠ s in 𝓝 t, J s = J t) ∨ (∀ᶠ s in 𝓝 t, q s = 1))
    {T : ℝ} (hc0 : ∀ t ≤ T, c t = 1) (hq0 : ∀ t ≤ T, q t = 1) : SmoothMetric n where
…

    Mentions: OAI.HarmonicCounterexample.SmoothMetric

  54. lemma OAI.HarmonicCounterexample.Cartesian.bergerMetric_euclidean line 445
  55. lemma OAI.HarmonicCounterexample.Cartesian.rawCoefficient_radial line 461

    Source documentation

    The radial unit eigenvalue is exact, not just a uniform comparison.

    lemma rawCoefficient_radial {n : ℕ} (c q : ℝ → ℝ)
    (J : ℝ → ComplexStructure (Fin n)) (x : Coord n) :
    rawCoefficient c q J x *ᵥ x = x := by
…

    Mentions: OAI.HarmonicCounterexample.Cartesian.Coord, OAI.HarmonicCounterexample.Cartesian.rawCoefficient

  56. lemma OAI.HarmonicCounterexample.coordDeriv_add line 490
  57. lemma OAI.HarmonicCounterexample.coordDeriv_sub line 495
  58. lemma OAI.HarmonicCounterexample.coordDeriv_mul line 500
  59. lemma OAI.HarmonicCounterexample.coordDeriv_const line 507
  60. lemma OAI.HarmonicCounterexample.coordDeriv_coordinate line 510
  61. lemma OAI.HarmonicCounterexample.coordDeriv_sum line 515
  62. lemma OAI.HarmonicCounterexample.coordDeriv_linear line 520
  63. lemma OAI.HarmonicCounterexample.coordDeriv_congr line 532
  64. lemma OAI.HarmonicCounterexample.coordDeriv_chain line 536
  65. lemma OAI.HarmonicCounterexample.coordDeriv_inv line 543
  66. lemma OAI.HarmonicCounterexample.coordDeriv_div line 548
  67. lemma OAI.HarmonicCounterexample.coordDeriv_pow line 558