OAI/Geometry/HarmonicGrowth/Main.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicCounterexample.Angular.regularValue line 14

   Source documentation

   The genuine center-regular ODE solution in the actual angular polynomial space.

   def regularValue (J : ℝ → ComplexStructure (Fin n)) (l : ℕ)
       (c q d : ℝ → ℝ) (P : harmonicPolynomials n l) (t : ℝ) : harmonicPolynomials n l :=
   …

   Mentions: OAI.HarmonicCounterexample.Angular.harmonicPolynomials

2. def OAI.HarmonicCounterexample.Angular.regularHarmonic line 19

   Source documentation

   Evaluating the actual global flow as a function on R^n.

   def regularHarmonic (B : Basis ι ℝ (harmonicPolynomials n l))
       (J : ℝ → ComplexStructure (Fin n)) (c q d : ℝ → ℝ)
       (P : harmonicPolynomials n l) : Space n → ℝ :=
   …

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

3. lemma OAI.HarmonicCounterexample.Angular.regularValue_core line 34
4. lemma OAI.HarmonicCounterexample.Angular.regularHarmonic_core line 43
5. lemma OAI.HarmonicCounterexample.Angular.regularHarmonic_smooth line 53
6. lemma OAI.HarmonicCounterexample.Angular.regularHarmonic_injective line 61
7. lemma OAI.HarmonicCounterexample.Angular.regularHarmonic_harmonic line 71
8. theorem OAI.HarmonicCounterexample.GlobalGrowth.absorb_compact line 127

   Source documentation

   Smoothness cannot by itself be substituted for the all-point growth bound. This compact absorption lemma supplies the missing uniform constant.

   theorem absorb_compact {E : Type*} [TopologicalSpace E]
       (u r : E → ℝ) (hu : Continuous u) (hr : ∀ x, 0 ≤ r x)
       (hcompact : ∀ R, IsCompact {x | r x ≤ R}) (k : ℕ)
       {D R : ℝ} (houtside : ∀ x, R ≤ r x → |u x| ≤ D * (1+r x)^k) :
       ∃ C : ℝ, 0 ≤ C ∧ ∀ x, |u x| ≤ C * (1+r x)^k := by
   …

9. theorem OAI.HarmonicCounterexample.GlobalGrowth.angular_bound line 149

   Source documentation

   The finite-dimensional angular norm estimate is uniform over the entire compact link, not just at a finite set of angles.

   theorem angular_bound {ι X : Type*} [Fintype ι] [TopologicalSpace X]
       (K : Set X) (hK : IsCompact K) (φ : ι → X → ℝ)
       (hφ : ∀ i, ContinuousOn (φ i) K) :
       ∃ C : ℝ, 0 ≤ C ∧ ∀ (y : ι → ℝ) (x : X), x ∈ K →
         |∑ i, y i * φ i x| ≤ C * ‖y‖ := by
   …

10. theorem OAI.HarmonicCounterexample.GlobalGrowth.independent_of_restriction line 175

    Source documentation

    Independence of restrictions implies independence of actual global functions; equality only on a fixed sphere suffices.

    theorem independent_of_restriction {ι X Y : Type*} (f : Y → X)
        (u : ι → X → ℝ) (h : LinearIndependent ℝ (fun i => u i ∘ f)) :
        LinearIndependent ℝ u := by
    …

11. lemma OAI.HarmonicCounterexample.Angular.normalized_point_norm line 196
12. lemma OAI.HarmonicCounterexample.Angular.synthesized_normalized line 204
13. lemma OAI.HarmonicCounterexample.Angular.synthesized_angular_bound line 218

    Source documentation

    A true uniform sphere estimate for every time of the actual polynomial synthesis, not a finite sampling of directions.

    lemma synthesized_angular_bound (B : Basis ι ℝ (harmonicPolynomials n l)) :
        ∃ C : ℝ, 0 ≤ C ∧ ∀ (Y : ℝ → ι → ℝ) (x : Space n), x ≠ 0 →
          |synthesized l (fun i => evaluate (B i : PolynomialSpace n)) Y x| ≤
            C * ‖Y (logRadius x)‖ := by
    …

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

14. lemma OAI.HarmonicCounterexample.Angular.synthesized_growth line 233

    Source documentation

    The all-point polynomial bound from a genuine coefficient-flow bound. The compact core is absorbed using the actual smooth global function.

    lemma synthesized_growth (B : Basis ι ℝ (harmonicPolynomials n l))
        (Y : ℝ → ι → ℝ) (k : ℕ)
        (hs : Continuous (synthesized l (fun i => evaluate (B i : PolynomialSpace n)) Y))
        {D T : ℝ} (hD : 0 ≤ D)
        (hY : ∀ t, T ≤ t → ‖Y t‖ ≤ D*Real.exp ((k:ℝ)*t)) :
        ∃ C : ℝ, 0 ≤ C ∧ ∀ x,
          |synthesized l (fun i => evaluate (B i : PolynomialSpace n)) Y x| ≤
            C*(1+radius x)^k := by
    …

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

15. lemma OAI.HarmonicCounterexample.Angular.independent_homogeneous_family line 270

    Source documentation

    Independence in distinct homogeneous degrees, retaining all coefficients.

    lemma independent_homogeneous_family {δ : Type*} [Fintype δ]
        {ι : δ → Type*} [∀ d,Fintype (ι d)] (degree : δ → ℕ)
        (hdegree : Function.Injective degree)
        (P : (d : δ) → ι d → PolynomialSpace n)
        (hP : ∀ d j,P d j ∈ homogeneousSubmodule (Fin n) ℝ (degree d))
        (hli : ∀ d,LinearIndependent ℝ (P d)) :
        LinearIndependent ℝ (fun i : Sigma ι => P i.1 i.2) := by
    …

    Mentions: OAI.HarmonicCounterexample.Angular.PolynomialSpace

16. def OAI.HarmonicCounterexample.Angular.coreEvaluation line 289

    Source documentation

    Evaluation on the whole open flat core, as an actual function space.

    def coreEvaluation : PolynomialSpace n →ₗ[ℝ]
        ({x : Space n // squareRadius x < 1} → ℝ) where
    …

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

17. lemma OAI.HarmonicCounterexample.Angular.coreEvaluation_injective line 295
18. def OAI.HarmonicCounterexample.Angular.coreRestriction line 301
19. lemma OAI.HarmonicCounterexample.Angular.independent_of_core line 309

    Source documentation

    Core independence proves independence of the global functions. No unproved unique-continuation principle is used.

    lemma independent_of_core {ι : Type*} (P : ι → PolynomialSpace n)
        (hP : LinearIndependent ℝ P) (f : ι → Space n → ℝ)
        (hf : ∀ i x,squareRadius x < 1 → f i x = evaluate (P i) x) :
        LinearIndependent ℝ f := by
    …

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

20. theorem OAI.HarmonicCounterexample.Angular.independent_across_degrees line 321

    Source documentation

    The complete finite-family independence bridge for the degree-by-degree center-regular harmonic producer in the manuscript.

    theorem independent_across_degrees {δ : Type*} [Fintype δ]
        {ι : δ → Type*} [∀ d,Fintype (ι d)] (degree : δ → ℕ)
        (hdegree : Function.Injective degree)
        (P : (d : δ) → ι d → harmonicPolynomials n (degree d))
        (hP : ∀ d,LinearIndependent ℝ (P d))
        (f : Sigma ι → Space n → ℝ)
        (hf : ∀ i x,squareRadius x < 1 → f i x = evaluate (P i.1 i.2) x) :
        LinearIndependent ℝ f := by
    …

    Mentions: OAI.HarmonicCounterexample.Angular.harmonicPolynomials, OAI.HarmonicCounterexample.Space, OAI.HarmonicCounterexample.Angular.evaluate

21. lemma OAI.HarmonicCounterexample.Construction.Stream.drift_core line 349
22. lemma OAI.HarmonicCounterexample.Construction.Stream.trajectory_regularValue line 353
23. def OAI.HarmonicCounterexample.Construction.Stream.harmonic line 360
24. lemma OAI.HarmonicCounterexample.Construction.Stream.harmonic_core line 363
25. lemma OAI.HarmonicCounterexample.Construction.Stream.harmonic_smooth line 369
26. lemma OAI.HarmonicCounterexample.Construction.Stream.metric_locally_one line 374
27. lemma OAI.HarmonicCounterexample.Construction.Stream.metric_inverse line 379
28. lemma OAI.HarmonicCounterexample.Construction.Stream.metric_connection line 392
29. lemma OAI.HarmonicCounterexample.Construction.Stream.harmonic_laplace line 403
30. lemma OAI.HarmonicCounterexample.Construction.Stream.harmonic_growth line 414
31. lemma OAI.HarmonicCounterexample.Construction.Stream.harmonic_member line 425
32. lemma OAI.HarmonicCounterexample.Construction.Stream.harmonic_independent line 433
33. lemma OAI.HarmonicCounterexample.Construction.selectedFamily_card line 451
34. lemma OAI.HarmonicCounterexample.Construction.embedding_of_strict_card line 454
35. def OAI.HarmonicCounterexample.Construction.familyEmbedding line 459
36. theorem OAI.HarmonicCounterexample.main line 475

    Source documentation

    The actual complete Ricci-nonnegative manifold and the actual polynomial- growth harmonic functions manufactured by the same globally admissible stream. This proves every clause of the unchanged manuscript main theorem.

    Distinct definitions of this name: ComparatorChallenges/HarmonicGrowth.lean:102 (same statement text; different proof or body). Qualify references as OAI.HarmonicCounterexample.main@path.

    theorem main : MainClaim := by
    …

    Mentions: OAI.HarmonicCounterexample.MainClaim