OAI/Geometry/HarmonicGrowth/Intrinsic.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicCounterexample.quadratic line 12

   Source documentation

   The exact coordinate quadratic form used by path length.

   def quadratic {n : ℕ} (g : SmoothMetric n) (x v : Space n) : ℝ :=
   …

   Mentions: OAI.HarmonicCounterexample.SmoothMetric, OAI.HarmonicCounterexample.Space

2. def OAI.HarmonicCounterexample.speed line 15
3. lemma OAI.HarmonicCounterexample.speed_continuous line 18
4. lemma OAI.HarmonicCounterexample.pathLength_nonneg line 29
5. lemma OAI.HarmonicCounterexample.pathLength_bddBelow line 35
6. lemma OAI.HarmonicCounterexample.line_smooth line 42
7. lemma OAI.HarmonicCounterexample.line_deriv line 45
8. lemma OAI.HarmonicCounterexample.pathLength_set_nonempty line 50
9. lemma OAI.HarmonicCounterexample.distance_nonneg line 55
10. lemma OAI.HarmonicCounterexample.norm_sub_le_length line 62

    Source documentation

    Lower length comparison is proved for every admitted path.

    lemma norm_sub_le_length {n : ℕ} (g : SmoothMetric n) {a : ℝ} (ha : 0 < a)
        (hlower : ∀ x v, a^2 * ‖v‖^2 ≤ quadratic g x v)
        {γ : ℝ → Space n} (hγ : ContDiff ℝ 1 γ) :
        ‖γ 1 - γ 0‖ ≤ pathLength g γ / a := by
    …

    Mentions: OAI.HarmonicCounterexample.SmoothMetric, OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.quadratic, OAI.HarmonicCounterexample.Space, OAI.HarmonicCounterexample.pathLength

11. lemma OAI.HarmonicCounterexample.lower_distance line 79
12. lemma OAI.HarmonicCounterexample.upper_distance line 88

    Source documentation

    Upper length comparison uses the genuine straight Cartesian path.

    lemma upper_distance {n : ℕ} (g : SmoothMetric n) {b : ℝ} (hb : 0 ≤ b)
        (hupper : ∀ x v, quadratic g x v ≤ b^2 * ‖v‖^2) (x y : Space n) :
        distance g x y ≤ b * ‖y-x‖ := by
    …

    Mentions: OAI.HarmonicCounterexample.SmoothMetric, OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.quadratic, OAI.HarmonicCounterexample.Space, OAI.HarmonicCounterexample.distance

13. theorem OAI.HarmonicCounterexample.complete_of_uniform_bounds line 112

    Source documentation

    Uniform equivalence with the Cartesian norm gives genuine intrinsic completeness, with the exact sequence definition in the frozen target.

    theorem complete_of_uniform_bounds {n : ℕ} (g : SmoothMetric n)
        {a b : ℝ} (ha : 0 < a) (hb : 0 < b)
        (hlower : ∀ x v, a^2 * ‖v‖^2 ≤ quadratic g x v)
        (hupper : ∀ x v, quadratic g x v ≤ b^2 * ‖v‖^2) : Complete g := by
    …

    Mentions: OAI.HarmonicCounterexample.SmoothMetric, OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.quadratic, OAI.HarmonicCounterexample.Complete

14. lemma OAI.HarmonicCounterexample.quadratic_eq_dot line 150
15. lemma OAI.HarmonicCounterexample.quadratic_nonneg line 159
16. lemma OAI.HarmonicCounterexample.radial_gram_bound line 166

    Source documentation

    Positivity and the exact radial eigenvector give the angular-gradient bound. This is a quadratic-form Cauchy-Schwarz argument, not geodesic lore.

    lemma radial_gram_bound {n : ℕ} (g : SmoothMetric n)
        (hrad : ∀ x, g.coeff x *ᵥ x = x) (x v : Space n) :
        (x ⬝ᵥ v)^2 ≤ squareRadius x * quadratic g x v := by
    …

    Mentions: OAI.HarmonicCounterexample.SmoothMetric, OAI.HarmonicCounterexample.Space, OAI.HarmonicCounterexample.quadratic

17. lemma OAI.HarmonicCounterexample.squareRadius_hasDerivAt line 191
18. lemma OAI.HarmonicCounterexample.regularized_radius_length line 206

    Source documentation

    Radius regularization removes the nondifferentiability at EVERY crossing of the origin, so the lower distance estimate applies to all admitted paths.

    lemma regularized_radius_length {n : ℕ} (g : SmoothMetric n)
        (hrad : ∀ x, g.coeff x *ᵥ x = x) {γ : ℝ → Space n}
        (hγ : ContDiff ℝ 1 γ) {ε : ℝ} (hε : 0 < ε) :
        |Real.sqrt (squareRadius (γ 1)+ε) - Real.sqrt (squareRadius (γ 0)+ε)| ≤
          pathLength g γ := by
    …

    Mentions: OAI.HarmonicCounterexample.SmoothMetric, OAI.HarmonicCounterexample.Space, OAI.HarmonicCounterexample.pathLength

19. lemma OAI.HarmonicCounterexample.radial_length_lower line 236
20. lemma OAI.HarmonicCounterexample.radius_le_distance line 251
21. lemma OAI.HarmonicCounterexample.radial_line_length line 259
22. theorem OAI.HarmonicCounterexample.distance_origin_eq_radius line 279

    Source documentation

    Exact intrinsic radial distance for the smooth polar extension.

    theorem distance_origin_eq_radius {n : ℕ} (g : SmoothMetric n)
        (hrad : ∀ x, g.coeff x *ᵥ x = x) (hzero : g.coeff 0 = 1) (x : Space n) :
        distance g 0 x = radius x := by
    …

    Mentions: OAI.HarmonicCounterexample.SmoothMetric, OAI.HarmonicCounterexample.Space, OAI.HarmonicCounterexample.distance

23. lemma OAI.HarmonicCounterexample.radius_smul line 299
24. def OAI.HarmonicCounterexample.radialBall line 306
25. lemma OAI.HarmonicCounterexample.radialBall_measurable line 308
26. lemma OAI.HarmonicCounterexample.omega_eq_radialBall line 311
27. lemma OAI.HarmonicCounterexample.omega_pos line 321
28. lemma OAI.HarmonicCounterexample.omega_ne_top line 326
29. lemma OAI.HarmonicCounterexample.radialBall_scale line 333
30. lemma OAI.HarmonicCounterexample.radialBall_volume line 341
31. lemma OAI.HarmonicCounterexample.lintegral_comp_smul line 347
32. lemma OAI.HarmonicCounterexample.radial_integral_scale line 361

    Source documentation

    Change of variables is carried out on the actual Cartesian volume, not an assumed polar volume formula.

    lemma radial_integral_scale {n : ℕ} {R : ℝ} (hR : 0 < R)
        (f : Space n → ℝ≥0∞) :
        (∫⁻ x in radialBall n R, f x ∂volume) = ENNReal.ofReal (R^n) *
          ∫⁻ x in radialBall n 1, f (R • x) ∂volume := by
    …

    Mentions: OAI.HarmonicCounterexample.Space, OAI.HarmonicCounterexample.radialBall

33. lemma OAI.HarmonicCounterexample.radial_integral_ratio line 380
34. theorem OAI.HarmonicCounterexample.radial_integral_ratio_limit line 400

    Source documentation

    A change-of-variables dominated convergence proof of the actual Cartesian volume-ratio limit. The only exceptional ray is the null singleton at the origin.

    theorem radial_integral_ratio_limit {n : ℕ} (hn : 0 < n)
        {f : Space n → ℝ≥0∞} (hf : Measurable f) {C A : ℝ≥0∞}
        (hC : C ≠ (∞ : ℝ≥0∞)) (hbound : ∀ x, f x ≤ C)
        (hlim : ∀ x ≠ 0, Tendsto (fun R : ℝ => f (R • x)) atTop (𝓝 A)) :
        Tendsto (fun R : ℝ => (∫⁻ x in radialBall n R, f x ∂volume) /
          (omega n * ENNReal.ofReal (R^n))) atTop (𝓝 A) := by
    …

    Mentions: OAI.HarmonicCounterexample.Space, OAI.HarmonicCounterexample.radialBall, OAI.HarmonicCounterexample.omega

35. lemma OAI.HarmonicCounterexample.profile_scaling_limit line 429

    Source documentation

    Radial profiles converging along logarithmic radius converge on every nonzero dilated ray, with no assertion at the origin.

    lemma profile_scaling_limit {n : ℕ} {a : ℝ → ℝ} {A : ℝ}
        (ha : Tendsto a atTop (𝓝 A)) {x : Space n} (hx : x ≠ 0) :
        Tendsto (fun R : ℝ => a (logRadius (R • x))) atTop (𝓝 A) := by
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.Space

36. theorem OAI.HarmonicCounterexample.metric_avr_of_density line 440

    Source documentation

    Abstract geometric interface for the exact metric volume definition.

    theorem metric_avr_of_density {n : ℕ} (hn : 0 < n) (g : SmoothMetric n)
        (hd : ∀ x, distance g 0 x = radius x) {A C : ℝ}
        (hA : 0 < A) (hA1 : A < 1)
        (hC : ∀ x, Real.sqrt (g.coeff x).det ≤ C)
        (hlim : ∀ x ≠ 0, Tendsto
          (fun R : ℝ => Real.sqrt (g.coeff (R • x)).det) atTop (𝓝 A)) :
        PositiveSubunitAVR g := by
    …

    Mentions: OAI.HarmonicCounterexample.SmoothMetric, OAI.HarmonicCounterexample.distance, OAI.HarmonicCounterexample.PositiveSubunitAVR

37. lemma OAI.HarmonicCounterexample.Berger.det_one_add_rank_one line 469
38. lemma OAI.HarmonicCounterexample.Berger.det_one_add_scalar_projector line 477
39. lemma OAI.HarmonicCounterexample.Berger.tensor_factorization line 484
40. theorem OAI.HarmonicCounterexample.Berger.tensor_det line 498

    Source documentation

    Exact volume density before the volume-normalizing choice c=a²q^(-1/m). No orientation choice appears in the determinant.

    theorem tensor_det {u v : ι → ℝ}
        (hu : u ⬝ᵥ u = 1) (hv : v ⬝ᵥ v = 1) (huv : u ⬝ᵥ v = 0)
        {c : ℝ} (hc : c ≠ 0) (q : ℝ) :
        (tensor u v c q).det = c ^ Fintype.card ι * c⁻¹ * q := by
    …

    Mentions: OAI.HarmonicCounterexample.Berger.tensor

41. def OAI.HarmonicCounterexample.Berger.horizontalFactor line 507

    Source documentation

    The source normalization keeps the angular volume unchanged by q.

    def horizontalFactor (m : ℕ) (a q : ℝ) : ℝ := a^2 * q^((-1:ℝ)/(m:ℝ))

    Mentions: OAI.HarmonicCounterexample.a

42. lemma OAI.HarmonicCounterexample.Berger.horizontalFactor_pos line 509
43. lemma OAI.HarmonicCounterexample.Berger.horizontalFactor_normalization line 513
44. theorem OAI.HarmonicCounterexample.Berger.normalized_tensor_det line 523

    Source documentation

    The determinant and square-root volume density in dimension m+1 are exact, including every intermediate orientation and both signs of pulses.

    theorem normalized_tensor_det {m : ℕ} (hm : m ≠ 0)
        {u v : Fin (m+1) → ℝ} (hu : u ⬝ᵥ u = 1) (hv : v ⬝ᵥ v = 1)
        (huv : u ⬝ᵥ v = 0) {a q : ℝ} (ha : 0 < a) (hq : 0 < q) :
        (tensor u v (horizontalFactor m a q) q).det = a^(2*m) := by
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.Berger.tensor, OAI.HarmonicCounterexample.Berger.horizontalFactor

45. lemma OAI.HarmonicCounterexample.Berger.normalized_tensor_density line 532
46. lemma OAI.HarmonicCounterexample.Berger.tensor_upper_bound line 548
47. lemma OAI.HarmonicCounterexample.Construction.scale_uniform_bounds line 569
48. lemma OAI.HarmonicCounterexample.Cartesian.squareRadius_le_norm line 599
49. lemma OAI.HarmonicCounterexample.Cartesian.rawCoefficient_uniform_bounds line 607
50. lemma OAI.HarmonicCounterexample.Construction.rawCoefficient_density line 655
51. theorem OAI.HarmonicCounterexample.Construction.profile_metric_global line 665

    Source documentation

    Completeness, exact radial distance and positive subunit AVR for the actual Cartesian tensor, with no ellipticity or volume conclusion left as a hypothesis.

    theorem profile_metric_global {μ : ℝ} (hμ : 0≤μ)
        {q : ℝ → ℝ} (hq : ContDiff ℝ ∞ q) (hqb : ∀ t,q t ∈ Icc (1/2:ℝ) 2)
        (J : ℝ → ComplexStructure (Fin 16))
        (hJ : ∀ t,(∀ᶠ u in 𝓝 t,J u=J t) ∨ (∀ᶠ u in 𝓝 t,q u=1))
        (hc0 : ∀ t≤0,horizontalScale μ q t=1) (hq0 : ∀ t≤0,q t=1)
        (ha : Tendsto (Scale.profile μ) atTop (𝓝 a)) :
        let hqp : ∀ t,0<q t := fun t => lt_of_lt_of_le (by norm_num) (hqb t).1
    …

    Mentions: OAI.HarmonicCounterexample.Construction.horizontalScale, OAI.HarmonicCounterexample.Scale.profile, OAI.HarmonicCounterexample.Construction.a