OAI/Dynamics/ThreeTorus/RetainedPackets.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThreeTorus.integral_passageChart line 15
2. lemma OAI.ThreeTorus.physical_retainedPassage_error_le line 26

   Source documentation

   A complete quantitative form of the physical transport estimate (2.9). The sole right-hand quantity is the actual summed Fourier-mass error.

   lemma physical_retainedPassage_error_le {m : ℤ} {H : UnitAddCircle → UnitAddCircle}
       {A : UnitAddCircle × UnitAddCircle → ℂ} (hH : Continuous H) (hA : Continuous A)
       (S : Finset ℤ) (χ W : ℤ → UnitAddCircle → ℝ) (hχc : ∀ j, Continuous (χ j))
       (ψ : UnitAddCircle → ℝ) (hψc : Continuous ψ) (hψ : ∀ a, 0 ≤ ψ a ∧ ψ a ≤ 1)
       (hχ : ∀ j a, 0 ≤ χ j a ∧ χ j a ≤ 1)
       (hW : ∀ j a, W j a ≠ 0 → j ∈ S ∧ χ j a = 1)
       (hE : ∀ j, Integrable (fun a => |‖exactPassageCoeff m H A j a‖^2-W j a|)
         AddCircle.haarAddCircle)
       (hp : ∀ᵐ a ∂AddCircle.haarAddCircle,
         Summable (fun j => |‖exactPassageCoeff m H A j a‖^2-W j a|))
       (hs : Summable (fun j => ∫ a, |‖exactPassageCoeff m H A j a‖^2-W j a|
         ∂AddCircle.haarAddCircle)) :
   …

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

3. lemma OAI.ThreeTorus.pointwise_array_mass_error_summable line 78
4. lemma OAI.ThreeTorus.physical_retainedPassage_tendsto line 96

   Source documentation

   The actual physical packet cutoff error tends to zero once the unrounded stationary mass theorem is applied. All summability hypotheses are derived.

   lemma physical_retainedPassage_tendsto
       {m : ℤ} {H : ℕ → UnitAddCircle → UnitAddCircle}
       {A : UnitAddCircle × UnitAddCircle → ℂ} {W : ℝ → UnitAddCircle → ℝ}
       (hH : ∀ n, Continuous (H n)) (hA : Continuous A)
       (hWc : Continuous W.uncurry) (hWk : HasCompactSupport W.uncurry)
       (S : ℕ → Finset ℤ) (χ : ℕ → ℤ → UnitAddCircle → ℝ)
       (hχc : ∀ n j, Continuous (χ n j)) (hχ : ∀ n j a, 0 ≤ χ n j a ∧ χ n j a ≤ 1)
       (ψ : UnitAddCircle → ℝ) (hψc : Continuous ψ) (hψ : ∀ a, 0 ≤ ψ a ∧ ψ a ≤ 1)
       (hW : ∀ (n : ℕ), 0 < n → ∀ (j : ℤ) (a : UnitAddCircle), W ((j:ℝ)/n) a ≠ 0 → j ∈ S n ∧ χ n j a = 1)
       (ht : Tendsto (fun n : ℕ => ∑' j : ℤ, ∫ a : UnitAddCircle,
         |‖exactPassageCoeff m (H n) A j a‖^2-(n:ℝ)⁻¹*W ((j:ℝ)/n) a|
           ∂AddCircle.haarAddCircle) atTop (𝓝 0)) :
   …

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

5. lemma OAI.ThreeTorus.exact_physical_retainedPassage_tendsto line 134

   Source documentation

   Physical transport for the actual signed packet. The summed stationary mass error is proved, not an input to this statement.

   lemma exact_physical_retainedPassage_tendsto
       {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

6. lemma OAI.ThreeTorus.stationaryWeight_cylinder_support line 185
7. lemma OAI.ThreeTorus.lifted_amplitude_compactSupport line 200
8. lemma OAI.ThreeTorus.retained_amplitude_disjoint line 212

   Source documentation

   The output amplitudes from different colors are exactly disjoint at each shared angular index; asymptotic orthogonality is not used here.

   lemma retained_amplitude_disjoint {χ ξ : ℝ × UnitAddCircle → ℝ}
       (hd : Disjoint (tsupport χ) (tsupport ξ)) (s : ℝ)
       (F G : UnitAddCircle × UnitAddCircle → ℂ) :
       Disjoint (tsupport (fun p : UnitAddCircle × UnitAddCircle => (χ (s,p.1):ℂ)*F p))
         (tsupport (fun p : UnitAddCircle × UnitAddCircle => (ξ (s,p.1):ℂ)*G p)) := by
   …

9. lemma OAI.ThreeTorus.norm_spare_character line 225
10. lemma OAI.ThreeTorus.colored_stationary_cutoffs line 231

    Source documentation

    The source's finite stationary-image support selection, including the zero-frequency exclusion and exact disjointness of the cutoffs.

    lemma colored_stationary_cutoffs {ι : Type*} [Finite ι]
        (m : ι → ℤ) (V : ℝ → ℝ) (I : Set ℝ)
        (K U : ι → Set (ℝ × UnitAddCircle))
        (hm : ∀ i, m i ≠ 0) (hV : Continuous V) (hi : InjOn V I)
        (hK : ∀ i, IsCompact (K i)) (hKI : ∀ i, K i ⊆ I ×ˢ univ)
        (hzero : ∀ x ∈ I, V x ≠ 0)
        (hsep : ∀ i j, ∀ x ∈ I, ∀ y ∈ I, (m i:ℝ)*V x = (m j:ℝ)*V y → m i = m j)
        (hdisj : ∀ i j, i ≠ j → m i = m j → Disjoint (K i) (K j))
        (hU : ∀ i, IsOpen (U i)) (hKU : ∀ i, stationaryImage (m i) V (K i) ⊆ U i) :
        ∃ χ : ι → ℝ × UnitAddCircle → ℝ,
          (∀ i, CylinderSmooth (χ i) ∧ HasCompactSupport (χ i) ∧ tsupport (χ i) ⊆ U i ∧
            (∀ p, 0 ≤ χ i p ∧ χ i p ≤ 1) ∧ (∀ a, χ i (0,a) = 0) ∧
    …

    Mentions: OAI.ThreeTorus.stationaryImage, OAI.ThreeTorus.CylinderSmooth

11. lemma OAI.ThreeTorus.simultaneous_retained_indices line 270
12. theorem OAI.ThreeTorus.colored_physical_passage line 287

    Source documentation

    Simultaneous physical transport with constructed, disjoint cylinder cutoffs. The limit is a consequence of the signed stationary-phase theorem for the actual Fourier coefficients, not an assumption on an auxiliary array.

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

    Mentions: OAI.ThreeTorus.H

13. theorem OAI.ThreeTorus.finite_disjoint_frequency_cutoffs line 355

    Source documentation

    The second support separation in the manuscript uses cutoffs in frequency alone, as opposed to the first passage's frequency/slow-coordinate cutoffs.

    theorem finite_disjoint_frequency_cutoffs {ι : Type*} [Finite ι]
        (K U : ι → Set ℝ) (hK : ∀ i, IsCompact (K i)) (hU : ∀ i, IsOpen (U i))
        (hKU : ∀ i, K i ⊆ U i) (hdisj : Pairwise (Disjoint on K)) :
        ∃ χ : ι → ℝ → ℝ,
          (∀ i, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (χ i) ∧ HasCompactSupport (χ i) ∧
            tsupport (χ i) ⊆ U i ∧ (∀ s, 0 ≤ χ i s ∧ χ i s ≤ 1) ∧
            ∀ s ∈ K i, χ i =ᶠ[𝓝 s] 1) ∧
          Pairwise (fun i j => Disjoint (tsupport (χ i)) (tsupport (χ j))) := by
    …

14. lemma OAI.ThreeTorus.compactSupport_frequency_cylinder line 376
15. theorem OAI.ThreeTorus.disjoint_frequency_indices line 385

    Source documentation

    Sampling disjoint frequency supports gives exactly disjoint finite index sets. There is no asymptotic assertion in this exact separation conclusion.

    theorem disjoint_frequency_indices {ι : Type*}
        (χ : ι → ℝ → ℝ) (hc : ∀ i, HasCompactSupport (χ i)) (hz : ∀ i, χ i 0 = 0)
        (hd : Pairwise (fun i j => Disjoint (tsupport (χ i)) (tsupport (χ j)))) :
        ∃ S : ℕ → ι → Finset ℤ,
          (∀ n i, (0:ℤ) ∉ S n i) ∧
          (∀ n, Pairwise (fun i j => Disjoint (S n i) (S n j))) ∧
          ∀ n, 0 < n → ∀ i j, j ∈ S n i ↔ χ i ((j:ℝ)/n) ≠ 0 := by
    …

16. lemma OAI.ThreeTorus.frequency_images_disjoint line 420

    Source documentation

    Compact slow-coordinate supports at equal old index stay disjoint under strictly monotone stationary maps. Distinct indices use the separated ranges.

    lemma frequency_images_disjoint {ι : Type*} (m : ι → ℤ) (V : ℝ → ℝ)
        (I : Set ℝ) (K : ι → Set ℝ) (hm : ∀ i, m i ≠ 0) (hi : InjOn V I)
        (hKI : ∀ i, K i ⊆ I)
        (hsep : ∀ i j, ∀ x ∈ I, ∀ y ∈ I, (m i:ℝ)*V x = (m j:ℝ)*V y → m i = m j)
        (hdisj : ∀ i j, i ≠ j → m i = m j → Disjoint (K i) (K j)) :
        Pairwise (fun i j => Disjoint ((fun x => (m i:ℝ)*V x) '' K i)
          ((fun x => (m j:ℝ)*V x) '' K j)) := by
    …

17. theorem OAI.ThreeTorus.second_separation_cutoffs line 440

    Source documentation

    Full exact producer for the second passage's cutoff and index geometry.

    theorem second_separation_cutoffs {ι : Type*} [Finite ι]
        (m : ι → ℤ) (V : ℝ → ℝ) (I : Set ℝ) (K U : ι → Set ℝ)
        (hm : ∀ i, m i ≠ 0) (hV : Continuous V) (hi : InjOn V I)
        (hK : ∀ i, IsCompact (K i)) (hKI : ∀ i, K i ⊆ I)
        (hzero : ∀ x ∈ I, V x ≠ 0)
        (hsep : ∀ i j, ∀ x ∈ I, ∀ y ∈ I, (m i:ℝ)*V x = (m j:ℝ)*V y → m i = m j)
        (hdisj : ∀ i j, i ≠ j → m i = m j → Disjoint (K i) (K j))
        (hU : ∀ i, IsOpen (U i)) (hKU : ∀ i, (fun x => (m i:ℝ)*V x) '' K i ⊆ U i) :
        ∃ (χ : ι → ℝ → ℝ) (S : ℕ → ι → Finset ℤ),
          (∀ i, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (χ i) ∧ HasCompactSupport (χ i) ∧
            tsupport (χ i) ⊆ U i ∧ (∀ s, 0 ≤ χ i s ∧ χ i s ≤ 1) ∧
            ∀ s ∈ (fun x => (m i:ℝ)*V x) '' K i, χ i =ᶠ[𝓝 s] 1) ∧
    …

18. lemma OAI.ThreeTorus.CompactParameter.hasFDerivAt_compact_integral line 483

    Source documentation

    Compact-parameter differentiation, used by the exact passage near epsilon=0.

    lemma hasFDerivAt_compact_integral
        {E : Type} {G : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
        [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G]
        {F : E × ℝ → G} (hF : ContDiff ℝ 1 F) (a b : ℝ) (x : E) :
        HasFDerivAt (fun y => ∫ t in a..b, F (y,t))
          (∫ t in a..b, (fderiv ℝ F (x,t)).comp (ContinuousLinearMap.inl ℝ E ℝ)) x := by
    …

19. lemma OAI.ThreeTorus.CompactParameter.contDiff_compact_integral line 508

    Source documentation

    Smooth parameter integration over a fixed compact interval.

    lemma contDiff_compact_integral
        {E : Type} {G : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
        [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G]
        (n : ℕ) {F : E × ℝ → G} (hF : ContDiff ℝ n F) (a b : ℝ) :
        ContDiff ℝ n (fun y => ∫ t in a..b, F (y,t)) := by
    …

20. lemma OAI.ThreeTorus.CompactParameter.smooth_compact_integral line 533
21. lemma OAI.ThreeTorus.smooth_fourierCoeff_param line 546

    Source documentation

    Smoothness of a Fourier coefficient in an arbitrary finite-dimensional parameter, obtained from a compact interval integral of the literal lift.

    lemma smooth_fourierCoeff_param {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E]
        [FiniteDimensional ℝ E] {f : E → UnitAddCircle → ℂ}
        (hf : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
          (fun p : E × ℝ => f p.1 (p.2 : UnitAddCircle))) (j : ℤ) :
        ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (fun x => fourierCoeff (f x) j) := by
    …

22. lemma OAI.ThreeTorus.smooth_fourier_lift line 562
23. lemma OAI.ThreeTorus.smooth_exactPassageCoeff line 570

    Source documentation

    Smoothness of the exact old-amplitude coefficients; no stationary-phase approximation replaces these coefficients.

    lemma smooth_exactPassageCoeff {m : ℤ} {H : UnitAddCircle → UnitAddCircle}
        {Hl : ℝ → ℝ} {A : UnitAddCircle × UnitAddCircle → ℂ}
        (hHl : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) Hl)
        (hH : ∀ t : ℝ, H (t : UnitAddCircle) = (Hl t : UnitAddCircle))
        (hA : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
          (fun p : ℝ × ℝ => A (p.1,p.2))) (j : ℤ) :
        ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
          (fun a : ℝ => exactPassageCoeff m H A j a) := by
    …

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

24. lemma OAI.ThreeTorus.smooth_retained_amplitude line 585

    Source documentation

    The new amplitudes retained by the passage lie in the same smooth packet class needed for its next use.

    lemma smooth_retained_amplitude {m j : ℤ} {H : UnitAddCircle → UnitAddCircle}
        {Hl : ℝ → ℝ} {A : UnitAddCircle × UnitAddCircle → ℂ}
        {χ : ℝ × UnitAddCircle → ℝ} {ψ : UnitAddCircle → ℝ} (s : ℝ)
        (hHl : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) Hl)
        (hH : ∀ t : ℝ, H (t : UnitAddCircle) = (Hl t : UnitAddCircle))
        (hA : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (fun p : ℝ × ℝ => A (p.1,p.2)))
        (hχ : CylinderSmooth χ)
        (hψ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (fun a : ℝ => ψ a)) :
        ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (fun p : ℝ × ℝ =>
          (χ (s,p.1):ℂ)*(ψ p.1:ℂ)*exactPassageCoeff m H A j p.1*fourier m (p.2:UnitAddCircle)) := by
    …

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

25. lemma OAI.ThreeTorus.positive_density_map_of_vectorMeasure line 611

    Source documentation

    A nonnegative integrable density identity proved with signed vector measures is the identical ordinary measure identity.

    lemma positive_density_map_of_vectorMeasure
        {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
        {μ : Measure X} {ν : Measure Y} {f : X → Y} {q : X → ℝ} {p : Y → ℝ}
        (hf : Measurable f) (hq : Integrable q μ) (hp : Integrable p ν)
        (hq0 : ∀ x, 0 ≤ q x) (hp0 : ∀ y, 0 ≤ p y)
        (he : (μ.withDensityᵥ q).map f = ν.withDensityᵥ p) :
        (μ.withDensity (fun x => ENNReal.ofReal (q x))).map f =
          ν.withDensity (fun y => ENNReal.ofReal (p y)) := by
    …

    Mentions: OAI.ThreeTorus.μ

26. lemma OAI.ThreeTorus.branchDensity_nonneg line 628
27. lemma OAI.ThreeTorus.unfoldedModeDensity_nonneg line 636
28. lemma OAI.ThreeTorus.foldCircleDensity_nonneg line 643
29. def OAI.ThreeTorus.retainedAmplitude line 649

    Source documentation

    The literal new amplitude at a retained angular mode.

    def retainedAmplitude (ψ : UnitAddCircle → ℝ) (χ : ℝ → UnitAddCircle → ℝ)
        (m : ℤ) (H : ℕ → UnitAddCircle → UnitAddCircle)
        (A : UnitAddCircle × UnitAddCircle → ℂ) (n : ℕ) (j : ℤ)
        (p : UnitAddCircle × UnitAddCircle) : ℂ :=
    …

    Mentions: OAI.ThreeTorus.H

30. lemma OAI.ThreeTorus.retainedPassage_eq_sum_packets line 655
31. lemma OAI.ThreeTorus.retainedAmplitude_norm_sq line 661
32. lemma OAI.ThreeTorus.retainedAmplitude_modulus line 670
33. lemma OAI.ThreeTorus.map_withDensity_comp line 679

    Source comment

    The same elementary identity used in the supplied whitening proof.

    lemma map_withDensity_comp {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
        (μ : Measure X) {ζ : X → Y} {w : Y → ℝ≥0∞}
        (hζ : Measurable ζ) (hw : Measurable w) :
        (μ.withDensity (w ∘ ζ)).map ζ = (μ.map ζ).withDensity w := by
    …

    Mentions: OAI.ThreeTorus.μ

34. lemma OAI.ThreeTorus.packetSpectralMeasure_of_modulus line 693

    Source documentation

    If a coefficient's modulus is independent of its spare coordinate, its literal packet spectral measure is the single-coordinate weighted image.

    lemma packetSpectralMeasure_of_modulus
        {φ : UnitAddCircle → UnitAddCircle} (hφ : Measurable φ) {j : ℤ}
        {B : UnitAddCircle × UnitAddCircle → ℂ} {q : UnitAddCircle → ℝ}
        (hq : Measurable q) (hB : ∀ p, ‖B p‖^2 = q p.1) :
        packetSpectralMeasure φ j B =
          (AddCircle.haarAddCircle.withDensity (fun a => ENNReal.ofReal (q a))).map
            (fun a => j • φ a) := by
    …

    Mentions: OAI.ThreeTorus.packetSpectralMeasure

35. lemma OAI.ThreeTorus.retainedCircleWeight_nonneg line 709
36. lemma OAI.ThreeTorus.circleDensityLift_nonneg line 713
37. lemma OAI.ThreeTorus.positive_foldedModeDensity_pushforward line 723

    Source documentation

    The folded branch is the ordinary (positive) spectral density, not just an identity of signed integrals.

    lemma positive_foldedModeDensity_pushforward {q : UnitAddCircle → ℝ} {q₀ J₀ : ℝ → ℝ}
        {J : UnitAddCircle → ℝ} {o : ℝ} {I : Set ℝ}
        (hq : Integrable q AddCircle.haarAddCircle) (hqm : Measurable q₀)
        (hq0 : ∀ a, 0 ≤ q a) (hq00 : ∀ x, 0 ≤ q₀ x)
        (hq₀ : ∀ x ∈ Ioc o (o+1), q (x : UnitAddCircle) = q₀ x)
        (hq₀s : support q₀ ⊆ Ioc o (o+1)) (hqs : support q₀ ⊆ I)
        (hj : Measurable J) (hJ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) J₀)
        (hJe : ∀ x ∈ I, J (x : UnitAddCircle) = J₀ x)
        (hIo : IsOpen I) (hinj : InjOn J₀ I) (hd : ∀ x ∈ I, deriv J₀ x ≠ 0)
        {n j : ℝ} (hn : 0 < n) (hjn : j ≠ 0) :
        (AddCircle.haarAddCircle.withDensity (fun a => ENNReal.ofReal (q a))).map
            (fun a => (((j+(j/n)*J a)/n : ℝ) : UnitAddCircle)) =
    …

38. lemma OAI.ThreeTorus.passage_speed_mode line 753
39. lemma OAI.ThreeTorus.packetSpectralMeasure_new_speed line 763

    Source documentation

    Any coefficient with the actual retained modulus has the displayed nonnegative folded density under the actual new twist.

    lemma packetSpectralMeasure_new_speed {q : UnitAddCircle → ℝ} {q₀ J₀ : ℝ → ℝ}
        {J : UnitAddCircle → ℝ} {o : ℝ} {I : Set ℝ}
        {B : UnitAddCircle × UnitAddCircle → ℂ}
        (hq : Integrable q AddCircle.haarAddCircle) (hqmeas : Measurable q) (hqm : Measurable q₀)
        (hB : ∀ p, ‖B p‖^2 = q p.1) (hq00 : ∀ x, 0 ≤ q₀ x)
        (hq₀ : ∀ x ∈ Ioc o (o+1), q (x : UnitAddCircle) = q₀ x)
        (hq₀s : support q₀ ⊆ Ioc o (o+1)) (hqs : support q₀ ⊆ I)
        (hj : Measurable J) (hJ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) J₀)
        (hJe : ∀ x ∈ I, J (x : UnitAddCircle) = J₀ x)
        (hIo : IsOpen I) (hinj : InjOn J₀ I) (hd : ∀ x ∈ I, deriv J₀ x ≠ 0)
        {n : ℝ} {j : ℤ} (hn : 0 < n) (hjn : j ≠ 0) :
        packetSpectralMeasure (fun a => (((1+J a/n)/n:ℝ):UnitAddCircle)) j B =
    …

    Mentions: OAI.ThreeTorus.packetSpectralMeasure

40. lemma OAI.ThreeTorus.retainedAmplitude_spectralDensity line 788

    Source documentation

    Density identity for the literal retained coefficient used by the passage. The only support hypothesis is that the cutoff lies on the chosen good branch.

    lemma retainedAmplitude_spectralDensity
        {ψ : UnitAddCircle → ℝ} {χ : ℝ → UnitAddCircle → ℝ}
        {m : ℤ} {H : ℕ → UnitAddCircle → UnitAddCircle} {A : UnitAddCircle × UnitAddCircle → ℂ}
        {J : UnitAddCircle → ℝ} {J₀ : ℝ → ℝ} {o : ℝ} {I : Set ℝ}
        (hψ : Continuous ψ) (hχ : Continuous χ.uncurry)
        (hH : ∀ n, Continuous (H n)) (hA : Continuous A)
        (hψs : ∀ x ∈ Ioc o (o+1), ψ (x:UnitAddCircle) ≠ 0 → x ∈ I)
        (hj : Measurable J) (hJ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) J₀)
        (hJe : ∀ x ∈ I, J (x:UnitAddCircle) = J₀ x)
        (hIo : IsOpen I) (hinj : InjOn J₀ I) (hd : ∀ x ∈ I, deriv J₀ x ≠ 0)
        {n : ℕ} {j : ℤ} (hn : 0 < n) (hjn : j ≠ 0) :
        packetSpectralMeasure (fun a => (((1+J a/n)/n:ℝ):UnitAddCircle)) j
    …

    Mentions: OAI.ThreeTorus.H, OAI.ThreeTorus.packetSpectralMeasure

41. lemma OAI.ThreeTorus.packet_twisted_pair_zero line 828
42. lemma OAI.ThreeTorus.disjoint_packet_list_correlation line 856

    Source documentation

    The spectral measure of a smooth disjoint packet list is the sum of the literal packet pushforwards, demonstrated by every bilateral Fourier moment.

    lemma disjoint_packet_list_correlation {ι : Type*} [Fintype ι]
        (m : ι → ℤ) (A : ι → UnitAddCircle × UnitAddCircle → ℂ)
        (hA : ∀ i, Continuous (A i)) {φ : UnitAddCircle → UnitAddCircle} (hφ : Continuous φ)
        (hd : ∀ i j, i ≠ j → m i = m j → Disjoint (support (A i)) (support (A j)))
        (n : ℤ) :
        (∫ x : TripleTorus, starRingEnd ℂ (∑ i, packet (m i) (A i) x)*
            (∑ i, packet (m i) (A i) (twistIter φ n x)) ∂tripleVolume) =
          ∑ i, ∫ z, fourier n z ∂packetSpectralMeasure φ (m i) (A i) := by
    …

    Mentions: OAI.ThreeTorus.TripleTorus, OAI.ThreeTorus.packet, OAI.ThreeTorus.twistIter, OAI.ThreeTorus.tripleVolume, OAI.ThreeTorus.packetSpectralMeasure

43. lemma OAI.ThreeTorus.foldCircleDensity_add_ae line 904
44. lemma OAI.ThreeTorus.foldCircleDensity_finsetSum_ae line 919
45. lemma OAI.ThreeTorus.moment_withDensity_real line 939
46. lemma OAI.ThreeTorus.continuous_retainedAmplitude line 949
47. theorem OAI.ThreeTorus.retainedPassage_spectral_moment line 963

    Source documentation

    All bilateral Koopman moments of the actual finite retained vector are exactly those of its explicit nonnegative folded coefficient density.

    theorem retainedPassage_spectral_moment
        {ψ : UnitAddCircle → ℝ} {χ : ℝ → UnitAddCircle → ℝ}
        {m : ℤ} {H : ℕ → UnitAddCircle → UnitAddCircle} {A : UnitAddCircle × UnitAddCircle → ℂ}
        {J : UnitAddCircle → ℝ} {J₀ : ℝ → ℝ} {I : Set ℝ}
        (hψ : Continuous ψ) (hχ : Continuous χ.uncurry)
        (hH : ∀ n, Continuous (H n)) (hA : Continuous A)
        (hψs : ∀ x ∈ Ioc (0:ℝ) 1, ψ (x:UnitAddCircle) ≠ 0 → x ∈ I)
        (hj : Continuous J) (hJ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) J₀)
        (hJe : ∀ x ∈ I, J (x:UnitAddCircle) = J₀ x)
        (hIo : IsOpen I) (hinj : InjOn J₀ I) (hd : ∀ x ∈ I, deriv J₀ x ≠ 0)
        {n : ℕ} {S : Finset ℤ} (hn : 0 < n) (hS : ∀ j ∈ S, j ≠ 0) (k : ℤ) :
        let φ := fun a => (((1+J a/n)/n:ℝ):UnitAddCircle)
    …

    Mentions: OAI.ThreeTorus.H

48. lemma OAI.ThreeTorus.support_branchDensity_subset line 1049
49. lemma OAI.ThreeTorus.branchDensity_compact line 1060
50. lemma OAI.ThreeTorus.branchDensity_smooth line 1067
51. lemma OAI.ThreeTorus.unfoldedModeDensity_smooth line 1101
52. lemma OAI.ThreeTorus.unfoldedModeDensity_compact line 1115
53. lemma OAI.ThreeTorus.periodizedReal_eq_periodize line 1134
54. lemma OAI.ThreeTorus.foldCircleDensity_smooth_lift line 1153
55. def OAI.ThreeTorus.realRetainedWeight line 1166

    Source documentation

    The literal real lift of a retained coefficient weight. The smooth cutoff is taken before the final passage integer, as in the source.

    def realRetainedWeight (ψ₀ : ℝ → ℝ) (χ : ℝ → UnitAddCircle → ℝ)
        (m : ℤ) (H : ℕ → UnitAddCircle → UnitAddCircle)
        (A : UnitAddCircle × UnitAddCircle → ℂ) (n : ℕ) (j : ℤ) (x : ℝ) : ℝ :=
    …

    Mentions: OAI.ThreeTorus.H

56. lemma OAI.ThreeTorus.realRetainedWeight_support line 1171
57. lemma OAI.ThreeTorus.realRetainedWeight_compact line 1179
58. lemma OAI.ThreeTorus.realRetainedWeight_smooth line 1185
59. lemma OAI.ThreeTorus.retainedWeight_lift_eq line 1200
60. theorem OAI.ThreeTorus.exactRetainedPacketDensity_smooth_lift line 1216

    Source documentation

    Actual retained densities are smooth at all branch edges, including their zero set. This supplies the next passage's regularity; it is not an assumption that the density is already smooth.

    theorem exactRetainedPacketDensity_smooth_lift
        {I : Set ℝ} {J : ℝ → ℝ} {ψ : UnitAddCircle → ℝ} {ψ₀ : ℝ → ℝ}
        {χ : ℝ → UnitAddCircle → ℝ} {m : ℤ}
        {H : ℕ → UnitAddCircle → UnitAddCircle} {Hl : ℕ → ℝ → ℝ}
        {A : UnitAddCircle × UnitAddCircle → ℂ} {S : Finset ℤ} {n : ℕ}
        (hJ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) J) (hIo : IsOpen I)
        (hinj : InjOn J I) (hd : ∀ x ∈ I, deriv J x ≠ 0)
        (hψ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) ψ₀) (hc : HasCompactSupport ψ₀)
        (he : ∀ x ∈ Ioc (0:ℝ) (0+1), ψ (x:UnitAddCircle) = ψ₀ x)
        (hs : tsupport ψ₀ ⊆ Ioc (0:ℝ) (0+1) ∩ I)
        (hχ : CylinderSmooth χ.uncurry)
        (hHl : ∀ n, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (Hl n))
    …

    Mentions: OAI.ThreeTorus.H, OAI.ThreeTorus.CylinderSmooth

61. lemma OAI.ThreeTorus.continuous_of_continuous_lift line 1251
62. lemma OAI.ThreeTorus.positive_circle_branch_fold line 1269
63. lemma OAI.ThreeTorus.stationaryWeight_change_branch line 1301
64. theorem OAI.ThreeTorus.oldPacket_spectralDensity_of_modulus line 1311

    Source documentation

    The density of a literal old angular packet, not an abstract probability model. The integer speed carrier vanishes on the temporal circle.

    theorem oldPacket_spectralDensity_of_modulus
        {A : UnitAddCircle × UnitAddCircle → ℂ} {A₀ : ℝ → ℂ}
        {v : UnitAddCircle → ℝ} {V : ℝ → ℝ} {m c : ℤ} {o : ℝ} {C I : Set ℝ}
        (hA : Continuous A) (hA₀ : Continuous A₀)
        (hmod : ∀ u a, ‖A (u,a)‖ = ‖A (u,0)‖)
        (hAe : ∀ x ∈ Ioc o (o+1), A ((x:UnitAddCircle),0) = A₀ x)
        (has : support A₀ ⊆ Ioc o (o+1)) (hAs : support A₀ ⊆ I)
        (hv : Measurable v) (hV : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V)
        (hVe : ∀ x ∈ I, v (x:UnitAddCircle) = V x)
        (hIo : IsOpen I) (hIC : I ⊆ C) (hinj : InjOn (fun x => (m:ℝ)*V x) C)
        (hd : ∀ x ∈ I, deriv (fun x => (m:ℝ)*V x) x ≠ 0) :
        packetSpectralMeasure (fun a => ((v a-c:ℝ):UnitAddCircle)) m A =
    …

    Mentions: OAI.ThreeTorus.packetSpectralMeasure

65. lemma OAI.ThreeTorus.map_fst_withDensity_marginal line 1364
66. lemma OAI.ThreeTorus.continuous_slowMarginal line 1386
67. lemma OAI.ThreeTorus.packetSpectralMeasure_marginal line 1394
68. lemma OAI.ThreeTorus.branchDensity_integral line 1411
69. theorem OAI.ThreeTorus.oldPacket_spectralDensity line 1423

    Source documentation

    An arbitrary smooth/continuous old packet has the stationary marginal as its temporal density. Spare-coordinate independence is not required.

    theorem oldPacket_spectralDensity
        {A : UnitAddCircle × UnitAddCircle → ℂ} {A₀ : UnitAddCircle → ℝ → ℂ}
        {v : UnitAddCircle → ℝ} {V : ℝ → ℝ} {m c : ℤ} {o : ℝ} {C I : Set ℝ}
        (hA : Continuous A) (hA₀ : Continuous A₀.uncurry)
        (hAe : ∀ a x, x ∈ Ioc o (o+1) → A ((x:UnitAddCircle),a) = A₀ a x)
        (has : ∀ a, support (A₀ a) ⊆ Ioc o (o+1)) (hAs : ∀ a, support (A₀ a) ⊆ I)
        (hv : Measurable v) (hV : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V)
        (hVe : ∀ x ∈ I, v (x:UnitAddCircle) = V x)
        (hIo : IsOpen I) (hIC : I ⊆ C) (hinj : InjOn (fun x => (m:ℝ)*V x) C)
        (hd : ∀ x ∈ I, deriv (fun x => (m:ℝ)*V x) x ≠ 0) :
        packetSpectralMeasure (fun a => ((v a-c:ℝ):UnitAddCircle)) m A =
          AddCircle.haarAddCircle.withDensity (fun z => ENNReal.ofReal
    …

    Mentions: OAI.ThreeTorus.packetSpectralMeasure

70. lemma OAI.ThreeTorus.signed_circle_branch_fold line 1500
71. theorem OAI.ThreeTorus.oldStationaryMarginal_map line 1530
72. lemma OAI.ThreeTorus.cutoff_slowMarginal_l1 line 1595
73. theorem OAI.ThreeTorus.oldStationaryMarginal_cutoff_l1 line 1642

    Source documentation

    The reference in the neutral Riemann estimate is genuinely the cutoff old spectrum. Its loss is bounded independently of slope, residue modulus or passage integer.

    theorem oldStationaryMarginal_cutoff_l1
        {A : UnitAddCircle × UnitAddCircle → ℂ} {A₀ : UnitAddCircle → ℝ → ℂ}
        {v : UnitAddCircle → ℝ} {V : ℝ → ℝ} {m : ℤ} {o : ℝ} {C I : Set ℝ}
        (hA : Continuous A) (hA₀ : Continuous A₀.uncurry)
        (hAe : ∀ a x, x ∈ Ioc o (o+1) → A ((x:UnitAddCircle),a) = A₀ a x)
        (has : ∀ a, support (A₀ a) ⊆ Ioc o (o+1)) (hAs : ∀ a, support (A₀ a) ⊆ I)
        (hv : Measurable v) (hV : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V)
        (hVe : ∀ x ∈ I, v (x:UnitAddCircle) = V x)
        (hIo : IsOpen I) (hIC : I ⊆ C) (hinj : InjOn (fun x => (m:ℝ)*V x) C)
        (hd : ∀ x ∈ I, deriv (fun x => (m:ℝ)*V x) x ≠ 0)
        {ψ : UnitAddCircle → ℝ} (hψc : Continuous ψ) (hψ : ∀ a, 0 ≤ ψ a ∧ ψ a ≤ 1)
        {B : ℝ} (hB : 0 ≤ B) (hAb : ∀ p, ‖A p‖^2 ≤ B) :
    …

74. lemma OAI.ThreeTorus.sq_norm_sub_le_two line 1699
75. lemma OAI.ThreeTorus.continuous_passageChart line 1710
76. lemma OAI.ThreeTorus.continuous_retainedPassage line 1716
77. lemma OAI.ThreeTorus.cutoff_packet_error_eq line 1726
78. lemma OAI.ThreeTorus.cutoff_packet_error_le line 1748
79. lemma OAI.ThreeTorus.uncut_retainedPassage_error_le line 1770

    Source documentation

    Removing the good-arc cutoff adds no assumed physical approximation. Its missing mass is explicitly paid.

    lemma uncut_retainedPassage_error_le
        {A : UnitAddCircle × UnitAddCircle → ℂ} {m : ℤ}
        {H : ℕ → UnitAddCircle → UnitAddCircle} {χ : ℝ → UnitAddCircle → ℝ}
        (hA : Continuous A) (hH : ∀ n, Continuous (H n)) (hχ : Continuous χ.uncurry)
        (hmod : ∀ u a, ‖A (u,a)‖ = ‖A (u,0)‖) {δ : ℝ}
        (c : LawCutoffs δ) (hδ : 0 < δ) (hδ' : δ < 1/8) (n : ℕ) (S : Finset ℤ) :
        (∫ x : TripleTorus,
          ‖packet m A x-retainedPassage m (H n) A S (fun j => χ ((j:ℝ)/n))
            (neutralCircleCutoff c) (passageChart (H n) x)‖^2 ∂tripleVolume) ≤
          8*δ*(∫ u, ‖A (u,0)‖^2 ∂AddCircle.haarAddCircle)+
          2*(∫ x : TripleTorus,
          ‖(neutralCircleCutoff c x.2.2:ℂ)*packet m A x-
    …

    Mentions: OAI.ThreeTorus.H, OAI.ThreeTorus.LawCutoffs, OAI.ThreeTorus.TripleTorus, OAI.ThreeTorus.packet, OAI.ThreeTorus.retainedPassage, OAI.ThreeTorus.neutralCircleCutoff, OAI.ThreeTorus.passageChart, OAI.ThreeTorus.tripleVolume

80. theorem OAI.ThreeTorus.exact_quantile_passage line 1815

    Source documentation

    A single actual quantile passage simultaneously satisfies the physical, spectral, smoothness and all bilateral-moment conclusions. The passage integer remains arbitrarily large after the law, cutoffs and amplitudes are fixed.

    theorem exact_quantile_passage
        {A : UnitAddCircle × UnitAddCircle → ℂ} {A₀ : UnitAddCircle → ℝ → ℂ}
        {Pr V : ℝ → ℝ} {m : ℤ} {Δ : ℕ → ℝ} {H : ℕ → UnitAddCircle → UnitAddCircle}
        {o l u R : ℝ}
        (hm : m ≠ 0)
        (hH : ∀ n (x : ℝ), H n (x : UnitAddCircle) = ((n:ℝ)*(Pr 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))
        (hAr : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
          (fun p : ℝ × ℝ => A₀ (p.2 : UnitAddCircle) p.1))
        (hsupp : ∀ a, support (A₀ a) ⊆ Ioc l u)
    …

    Mentions: OAI.ThreeTorus.H

81. lemma OAI.ThreeTorus.continuous_stationaryWeight_parameter line 1926
82. lemma OAI.ThreeTorus.stationaryCutoffLift_marginal line 1937
83. lemma OAI.ThreeTorus.packet_cutoff_error_uniform line 1960
84. lemma OAI.ThreeTorus.packet_neutral_cutoff_error line 1998
85. lemma OAI.ThreeTorus.uncut_retainedPassage_uniform_error line 2007
86. theorem OAI.ThreeTorus.exact_neutral_passage line 2062