OAI/Dynamics/ThreeTorus/PassageMass.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThreeTorus.continuous_fourierCoeff_param line 17
2. def OAI.ThreeTorus.passageFourierInput line 28

   Source documentation

   The precise old-amplitude Fourier coefficients in the passage chart.

   def passageFourierInput (m : ℤ) (H : UnitAddCircle → UnitAddCircle)
       (A : UnitAddCircle × UnitAddCircle → ℂ) (a θ : UnitAddCircle) : ℂ :=
   …

   Mentions: OAI.ThreeTorus.H

3. def OAI.ThreeTorus.exactPassageCoeff line 32
4. def OAI.ThreeTorus.retainedPassage line 36
5. lemma OAI.ThreeTorus.continuous_passageFourierInput line 42
6. lemma OAI.ThreeTorus.continuous_exactPassageCoeff line 47
7. lemma OAI.ThreeTorus.packet_in_passage_chart line 52
8. lemma OAI.ThreeTorus.retainedPassage_error_norm line 61
9. lemma OAI.ThreeTorus.integrated_retainedPassage_error line 83
10. lemma OAI.ThreeTorus.exactPassageCoeff_real_integral line 133

    Source documentation

    The exact torus coefficient as a compactly supported real oscillatory integral. The support hypothesis is the lifted good-arc support, not a Fourier approximation.

    lemma exactPassageCoeff_real_integral {m j : ℤ} {H : UnitAddCircle → UnitAddCircle}
        {A : UnitAddCircle × UnitAddCircle → ℂ} {a : UnitAddCircle} {o : ℝ}
        {H₀ : ℝ → ℝ} {A₀ : ℝ → ℂ}
        (hH : ∀ x : ℝ, H (x : UnitAddCircle) = (H₀ x : UnitAddCircle))
        (hA : ∀ x ∈ Ioc o (o+1), A ((x : UnitAddCircle),a) = A₀ x)
        (hAs : Function.support A₀ ⊆ Ioc o (o+1)) :
        exactPassageCoeff m H A j a =
          ∫ x : ℝ, A₀ x*Complex.exp (Complex.I*((2*Real.pi*((m:ℝ)*H₀ x-j*x)):ℝ)) := by
    …

    Mentions: OAI.ThreeTorus.H, OAI.ThreeTorus.H₀, OAI.ThreeTorus.exactPassageCoeff

11. lemma OAI.ThreeTorus.rounded_phase_normalization line 168

    Source documentation

    No approximation occurs when the rounded primitive is inserted in the phase. This is the normalization needed by the compact-support stationary-phase proof.

    lemma rounded_phase_normalization (m j : ℤ) {n : ℕ} (hn : n ≠ 0)
        (P : ℝ → ℝ) (δ : ℕ → ℝ) (x : ℝ) :
        2*Real.pi*((m:ℝ)*((n:ℝ)*(P x+δ n*x))-(j:ℝ)*x) =
          (n:ℝ)*((2*Real.pi*(m:ℝ)*P x)-
            ((2*Real.pi)*(j:ℝ)/(n:ℝ)-(2*Real.pi*(m:ℝ)*δ n))*x) := by
    …

12. lemma OAI.ThreeTorus.continuous_compact_phase_integral line 181
13. lemma OAI.ThreeTorus.continuous_passageCoefficient line 198
14. lemma OAI.ThreeTorus.continuous_passageLeading line 205
15. lemma OAI.ThreeTorus.exactPassageCoeff_summed_mass line 215

    Source documentation

    Strong summed stationary mass for the actual torus passage coefficients. All integrability in the slow parameter is derived from compact smooth data.

    lemma exactPassageCoeff_summed_mass
        {A : UnitAddCircle × UnitAddCircle → ℂ} {A₀ : UnitAddCircle → ℝ → ℂ}
        {P : ℝ → ℝ} {m : ℤ} {δ : ℕ → ℝ} {H : ℕ → UnitAddCircle → UnitAddCircle}
        {o l u R d D C₀ C₁ M M₁ C : ℝ}
        (hH : ∀ n (x : ℝ), H n (x : UnitAddCircle) = ((n:ℝ)*(P x+δ n*x) : UnitAddCircle))
        (hA : ∀ a x, x ∈ Ioc o (o+1) → A ((x : UnitAddCircle),a) = A₀ a x)
        (hA₀ : ∀ a, ContDiff ℝ 2 (A₀ a)) (hAc : Continuous A₀.uncurry)
        (hsupp : ∀ a, Function.support (A₀ a) ⊆ Ioc l u)
        (hlo : o ≤ l) (huo : u ≤ o+1) (hlu : l ≤ u)
        (hΦ : ContDiff ℝ 3 (fun x => 2*Real.pi*(m:ℝ)*P x))
        (hR : 0 < R) (hd : 0 < d) (hdD : d ≤ D)
        (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hM₀ : 0 ≤ M) (hM₁ : 0 ≤ M₁) (hC : 0 ≤ C)
    …

    Mentions: OAI.ThreeTorus.H

16. def OAI.ThreeTorus.branchDensity line 270

    Source documentation

    Zero-extended Jacobian density on a single injective good arc.

    def branchDensity (I : Set ℝ) (J g D q : ℝ → ℝ) (y : ℝ) : ℝ :=
    …

17. lemma OAI.ThreeTorus.branchDensity_on line 273
18. def OAI.ThreeTorus.stationaryWeight line 279

    Source documentation

    The normalized physical-frequency mass used in (W-definition).

    def stationaryWeight (I : Set ℝ) (J : ℝ → ℝ) (A : ℝ → ℂ) : ℝ → ℝ :=
    …

19. lemma OAI.ThreeTorus.stationaryLeading_norm_sq_weight line 282
20. lemma OAI.ThreeTorus.phase_speed_derivatives line 319

    Source documentation

    Normalization of the phase derivative agrees exactly with the old speed. This computes the manuscript's W under the ordinary derivative identity P'=V.

    lemma phase_speed_derivatives {P V : ℝ → ℝ} {m : ℝ}
        (hP : Differentiable ℝ P) (hV : Differentiable ℝ V) (hPV : deriv P = V) :
        (∀ x, deriv (fun x => 2*Real.pi*m*P x) x = 2*Real.pi*(m*V x)) ∧
        (∀ x, iteratedDeriv 2 (fun x => 2*Real.pi*m*P x) x =
          2*Real.pi*deriv (fun x => m*V x) x) := by
    …

21. lemma OAI.ThreeTorus.exactPassageCoeff_summed_weight line 335

    Source documentation

    Summed stationary mass in the manuscript's actual normalization W, without an auxiliary complex leading array remaining in the conclusion.

    lemma exactPassageCoeff_summed_weight
        {A : UnitAddCircle × UnitAddCircle → ℂ} {A₀ : UnitAddCircle → ℝ → ℂ}
        {P V : ℝ → ℝ} {m : ℤ} {δ : ℕ → ℝ} {H : ℕ → UnitAddCircle → UnitAddCircle}
        {o l u R d D C₀ C₁ M M₁ C : ℝ}
        (hH : ∀ n (x : ℝ), H n (x : UnitAddCircle) = ((n:ℝ)*(P x+δ n*x) : UnitAddCircle))
        (hA : ∀ a x, x ∈ Ioc o (o+1) → A ((x : UnitAddCircle),a) = A₀ a x)
        (hA₀ : ∀ a, ContDiff ℝ 2 (A₀ a)) (hAc : Continuous A₀.uncurry)
        (hsupp : ∀ a, Function.support (A₀ a) ⊆ Ioc l u)
        (hlo : o ≤ l) (huo : u ≤ o+1) (hlu : l ≤ u)
        (hΦ : ContDiff ℝ 3 (fun x => 2*Real.pi*(m:ℝ)*P x))
        (hR : 0 < R) (hd : 0 < d) (hdD : d ≤ D)
        (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hM₀ : 0 ≤ M) (hM₁ : 0 ≤ M₁) (hC : 0 ≤ C)
    …

    Mentions: OAI.ThreeTorus.H

22. lemma OAI.ThreeTorus.continuous_fourier_summable line 386
23. lemma OAI.ThreeTorus.continuous_family_fourier_summable line 394

    Source documentation

    The integrated Fourier masses really are summable, so no use of a default zero value of a divergent tsum is possible in the passage estimates.

    lemma continuous_family_fourier_summable {f : UnitAddCircle → UnitAddCircle → ℂ}
        (hf : Continuous f.uncurry) :
        Summable (fun j : ℤ => ∫ a : UnitAddCircle, ‖fourierCoeff (f a) j‖^2
          ∂AddCircle.haarAddCircle) := by
    …

24. lemma OAI.ThreeTorus.exactPassageCoeff_summable line 420
25. lemma OAI.ThreeTorus.contDiffAt_invFunOn_of_deriv_ne_zero line 426
26. lemma OAI.ThreeTorus.isOpen_image_of_deriv_ne_zero line 452
27. def OAI.ThreeTorus.branchFamily line 473

    Source documentation

    The branch Jacobian with an arbitrary compact slow parameter space.

    def branchFamily {Ω : Type*} (I : Set ℝ) (J : ℝ → ℝ) (F : ℝ × Ω → ℝ)
        (p : ℝ × Ω) : ℝ := by
    …

28. lemma OAI.ThreeTorus.support_branchFamily_subset line 478
29. lemma OAI.ThreeTorus.branchFamily_compact line 491
30. lemma OAI.ThreeTorus.branchFamily_continuous line 499
31. lemma OAI.ThreeTorus.branchFamily_congr_branch line 540
32. lemma OAI.ThreeTorus.branchFamily_bound_first line 560
33. lemma OAI.ThreeTorus.stationaryWeight_family_eq line 573
34. lemma OAI.ThreeTorus.stationaryWeight_compact_continuous line 584

    Source documentation

    Joint compact continuity of the exact density used in stationary phase. The enlarged stationary branch creates no boundary discontinuity because the original packet is supported in the strictly smaller closed interval.

    lemma stationaryWeight_compact_continuous {J : ℝ → ℝ}
        {A : UnitAddCircle → ℝ → ℂ} {l u R : ℝ}
        (hJ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) J)
        (hA : Continuous A.uncurry) (hs : ∀ a, support (A a) ⊆ Icc l u)
        (hR : 0 < R) (hd : ∀ x ∈ Icc (l-R) (u+R), 0 < deriv J x) :
        Continuous (fun p : ℝ × UnitAddCircle => stationaryWeight (Icc (l-R) (u+R)) J (A p.2) p.1) ∧
        HasCompactSupport (fun p : ℝ × UnitAddCircle => stationaryWeight (Icc (l-R) (u+R)) J (A p.2) p.1) := by
    …

    Mentions: OAI.ThreeTorus.stationaryWeight

35. def OAI.ThreeTorus.roundingMass line 622
36. lemma OAI.ThreeTorus.roundingMass_bound line 626
37. lemma OAI.ThreeTorus.tendsto_roundingMass line 693

    Source documentation

    The rounding correction is removed at the coefficient mass level, without translating the actual lattice j/N or its fine phase.

    lemma tendsto_roundingMass {W : ℝ → UnitAddCircle → ℝ} {A C : ℝ} {L : ℝ≥0} {e : ℕ → ℝ}
        (hW : Continuous W.uncurry) (hLip : ∀ a, LipschitzWith L (fun s => W s a))
        (hs : ∀ s a, A < |s| → W s a = 0)
        (he : ∀ n, |e n| ≤ C) (ht : Tendsto e atTop (𝓝 0)) :
        Tendsto (fun n : ℕ => roundingMass W n (e n)) atTop (𝓝 0) := by
    …

    Mentions: OAI.ThreeTorus.roundingMass

38. lemma OAI.ThreeTorus.roundingMass_uniform_bound line 707
39. lemma OAI.ThreeTorus.tendsto_roundingMass_of_compact line 773

    Source documentation

    Compact continuity is sufficient for removal of rounding; no quantitative Lipschitz hypothesis has to be added to the old spectral density.

    lemma tendsto_roundingMass_of_compact {W : ℝ → UnitAddCircle → ℝ} {e : ℕ → ℝ}
        (hW : Continuous W.uncurry) (hc : HasCompactSupport W.uncurry)
        (ht : Tendsto e atTop (𝓝 0)) :
        Tendsto (fun n : ℕ => roundingMass W n (e n)) atTop (𝓝 0) := by
    …

    Mentions: OAI.ThreeTorus.roundingMass

40. lemma OAI.ThreeTorus.compact_lattice_support line 809
41. lemma OAI.ThreeTorus.compact_lattice_summable_integral line 829
42. lemma OAI.ThreeTorus.integrated_array_mass_error_summable line 838
43. lemma OAI.ThreeTorus.remove_array_rounding line 870

    Source documentation

    Removal of rounding for actual coefficient masses, with all summability proved from compact support and true squared Fourier mass.

    lemma remove_array_rounding {c : ℕ → ℤ → UnitAddCircle → ℂ}
        {W : ℝ → UnitAddCircle → ℝ} {e : ℕ → ℝ}
        (hW : Continuous W.uncurry) (hc : HasCompactSupport W.uncurry)
        (hcc : ∀ n j, Continuous (c n j))
        (hcs : ∀ n, Summable (fun j : ℤ => ∫ a : UnitAddCircle, ‖c n j a‖^2 ∂AddCircle.haarAddCircle))
        (he : Tendsto e atTop (𝓝 0))
        (ht : Tendsto (fun n => ∑' j : ℤ, ∫ a : UnitAddCircle,
          |‖c n j a‖^2-(n:ℝ)⁻¹*W ((j:ℝ)/n-e n) a| ∂AddCircle.haarAddCircle) atTop (𝓝 0)) :
        Tendsto (fun n => ∑' j : ℤ, ∫ a : UnitAddCircle,
          |‖c n j a‖^2-(n:ℝ)⁻¹*W ((j:ℝ)/n) a| ∂AddCircle.haarAddCircle) atTop (𝓝 0) := by
    …

44. lemma OAI.ThreeTorus.exactPassageCoeff_summed_unrounded line 928
45. lemma OAI.ThreeTorus.exactPassageCoeff_summed_positive line 983

    Source documentation

    A compact positive second derivative supplies every numerical constant used by the uniform stationary-phase estimate. None of those constants are extra hypotheses of the passage.

    lemma exactPassageCoeff_summed_positive
        {A : UnitAddCircle × UnitAddCircle → ℂ} {A₀ : UnitAddCircle → ℝ → ℂ}
        {P V : ℝ → ℝ} {m : ℤ} {δ : ℕ → ℝ} {H : ℕ → UnitAddCircle → UnitAddCircle}
        {o l u R : ℝ}
        (hm : 0 < m)
        (hH : ∀ n (x : ℝ), H n (x : UnitAddCircle) = ((n:ℝ)*(P x+δ n*x) : UnitAddCircle))
        (hA : ∀ a x, x ∈ Ioc o (o+1) → A ((x : UnitAddCircle),a) = A₀ a x)
        (hA₀ : ∀ a, ContDiff ℝ 2 (A₀ a)) (hAc : Continuous A₀.uncurry)
        (hAd : Continuous (fun p : UnitAddCircle × ℝ => deriv (A₀ p.1) p.2))
        (hsupp : ∀ a, Function.support (A₀ a) ⊆ Ioc l u)
        (hlo : o ≤ l) (huo : u ≤ o+1) (hlu : l ≤ u) (hR : 0 < R)
        (hP : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) P)
    …

    Mentions: OAI.ThreeTorus.H

46. lemma OAI.ThreeTorus.exactPassageCoeff_neg line 1065
47. lemma OAI.ThreeTorus.exactPassageCoeff_neg_norm line 1075
48. lemma OAI.ThreeTorus.summed_mass_reflect line 1081
49. lemma OAI.ThreeTorus.stationaryWeight_reflect line 1095
50. lemma OAI.ThreeTorus.exactPassageCoeff_summed line 1120

    Source documentation

    The source passage mass theorem at every nonzero angular index.

    lemma exactPassageCoeff_summed
        {A : UnitAddCircle × UnitAddCircle → ℂ} {A₀ : UnitAddCircle → ℝ → ℂ}
        {P V : ℝ → ℝ} {m : ℤ} {δ : ℕ → ℝ} {H : ℕ → UnitAddCircle → UnitAddCircle}
        {o l u R : ℝ}
        (hm : m ≠ 0)
        (hH : ∀ n (x : ℝ), H n (x : UnitAddCircle) = ((n:ℝ)*(P x+δ n*x) : UnitAddCircle))
        (hA : ∀ a x, x ∈ Ioc o (o+1) → A ((x : UnitAddCircle),a) = A₀ a x)
        (hA₀ : ∀ a, ContDiff ℝ 2 (A₀ a)) (hAc : Continuous A₀.uncurry)
        (hAd : Continuous (fun p : UnitAddCircle × ℝ => deriv (A₀ p.1) p.2))
        (hsupp : ∀ a, Function.support (A₀ a) ⊆ Ioc l u)
        (hlo : o ≤ l) (huo : u ≤ o+1) (hlu : l ≤ u) (hR : 0 < R)
        (hP : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) P)
    …

    Mentions: OAI.ThreeTorus.H