OAI/Dynamics/ThreeTorus/NeutralSupport.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThreeTorus.cell_sample_error line 14
2. lemma OAI.ThreeTorus.lattice_sample_error line 42

   Source documentation

   Arbitrary-offset unit lattice estimate, before scaling to the neutral refresh mesh.

   lemma lattice_sample_error {f : ℝ → ℝ} (hf : ContDiff ℝ 1 f)
       (hi : Integrable f) (hdi : Integrable (fun x => |deriv f x|)) (a : ℝ) :
       Summable (fun j : ℤ => f (a+j)) ∧
         |(∑' j : ℤ, f (a+j)) - ∫ x, f x| ≤ ∫ x, |deriv f x| := by
   …

3. lemma OAI.ThreeTorus.mesh_sample_error line 65

   Source documentation

   The mesh version of the arbitrary-offset Riemann estimate in neutral refresh.

   lemma mesh_sample_error {f : ℝ → ℝ} (hf : ContDiff ℝ 1 f)
       (hi : Integrable f) (hdi : Integrable (fun x => |deriv f x|))
       {h : ℝ} (hh : 0 < h) (a : ℝ) :
       Summable (fun j : ℤ => f (a+h*j)) ∧
         |h*(∑' j : ℤ, f (a+h*j)) - ∫ x, f x| ≤ h*∫ x, |deriv f x| := by
   …

4. lemma OAI.ThreeTorus.neutral_residue_riemann_error line 102

   Source documentation

   Exact normalization for a residue class of the neutral refresh lattice.

   lemma neutral_residue_riemann_error {f : ℝ → ℝ} (hf : ContDiff ℝ 1 f)
       (hi : Integrable f) (hdi : Integrable (fun x => |deriv f x|))
       {P s L : ℝ} (hP : 0 < P) (hs : 0 < s) (hL : 0 < L) (a : ℝ) :
       |(s*L)⁻¹*(∑' j : ℤ, f (a+P/(s*L)*j)) - P⁻¹*(∫ x, f x)|
         ≤ (s*L)⁻¹*(∫ x, |deriv f x|) := by
   …

5. lemma OAI.ThreeTorus.signed_mesh_sample_error line 127

   Source documentation

   Mesh reversal uses the actual integer negation bijection; negative old angular indices have the same arbitrary-offset Riemann estimate.

   lemma signed_mesh_sample_error {f : ℝ → ℝ} (hf : ContDiff ℝ 1 f)
       (hi : Integrable f) (hdi : Integrable (fun x => |deriv f x|))
       {h : ℝ} (hh : h ≠ 0) (a : ℝ) :
       Summable (fun j : ℤ => f (a+h*j)) ∧
         |(|h| *(∑' j : ℤ, f (a+h*j))) - ∫ x, f x| ≤ |h| *∫ x, |deriv f x| := by
   …

6. lemma OAI.ThreeTorus.signed_neutral_residue_error line 147

   Source documentation

   Exact signed normalization, with arbitrary offset and arbitrary positive integer residue spacing. This is source (neutral-riemann-error).

   lemma signed_neutral_residue_error {f : ℝ → ℝ} (hf : ContDiff ℝ 1 f)
       (hi : Integrable f) (hdi : Integrable (fun x => |deriv f x|))
       {P s L : ℝ} (hP : 0 < P) (hs : s ≠ 0) (hL : 0 < L) (y β : ℝ) :
       Summable (fun j : ℤ => (|s| *L)⁻¹*f (((y+j*P)/s-β)/L)) ∧
         |(∑' j : ℤ, (|s| *L)⁻¹*f (((y+j*P)/s-β)/L))-
             P⁻¹*(∫ a, f a)| ≤ (|s| *L)⁻¹*(∫ a, |deriv f a|) := by
   …

7. lemma OAI.ThreeTorus.fine_affine_neutral_error line 171
8. lemma OAI.ThreeTorus.compact_slice_tsupport line 200
9. lemma OAI.ThreeTorus.compact_slice_support line 208
10. lemma OAI.ThreeTorus.compact_slice_derivative_bound line 213
11. lemma OAI.ThreeTorus.compact_slice_integral_continuous line 245
12. lemma OAI.ThreeTorus.fine_affine_neutral_uniform line 254
13. lemma OAI.ThreeTorus.fine_affine_neutral_l1_error line 287
14. lemma OAI.ThreeTorus.compact_rect_bounds line 325
15. lemma OAI.ThreeTorus.neutral_fine_l1_bound line 346

    Source documentation

    Uniform residue equalization for actual compact smooth stationary weight. One slope is chosen before the passage integer, with all lattice phases, all residues, and both signs controlled.

    lemma neutral_fine_l1_bound {F : ℝ × ℝ → ℝ}
        (hF : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) F) (hcF : HasCompactSupport F)
        {ε : ℝ} (hε : 0 < ε) (hz : ∀ s a, |s| < ε → F (s,a) = 0) :
        ∃ C : ℝ, 0 ≤ C ∧ ∀ {P n : ℕ}, 0 < P → 0 < n → ∀ h : ℤ, ∀ L : ℝ, 0 < L → ∀ β : ℝ,
          (∫ s, |fineResidueKernel (affineKernel F L β) P h n s-
            (P:ℝ)⁻¹*(∫ a, F (s,a))|) ≤ C/L := by
    …

    Mentions: OAI.ThreeTorus.fineResidueKernel, OAI.ThreeTorus.affineKernel

16. lemma OAI.ThreeTorus.deriv_affine_on line 365
17. lemma OAI.ThreeTorus.branchKernel_affine_on line 375

    Source documentation

    The branch is the actual inverse of the affine jitter on the good arc. Off that image both sides vanish because the old stationary weight is cut off.

    lemma branchKernel_affine_on {I : Set ℝ} {J : ℝ → ℝ} {F : ℝ × ℝ → ℝ} {L β : ℝ}
        (hIo : IsOpen I) (hL : 0 < L) (he : ∀ a ∈ I, J a = L*a+β)
        (hs : tsupport F ⊆ I ×ˢ univ) (y s : ℝ) :
        branchKernel I J F (y,s) = L⁻¹*F ((y-β)/L,s) := by
    …

    Mentions: OAI.ThreeTorus.branchKernel

18. lemma OAI.ThreeTorus.passageBranchKernel_affine_on line 403
19. lemma OAI.ThreeTorus.compact_slice_integral_regular line 412
20. lemma OAI.ThreeTorus.affine_fine_regular line 423
21. lemma OAI.ThreeTorus.neutral_branch_circle_l1_bound line 440

    Source documentation

    The neutral equalization estimate on the actual temporal circle, uniformly in the large preparation integer, residues, offsets and affine good-arc jitter. The constant is fixed using only the old cut-off stationary weight.

    lemma neutral_branch_circle_l1_bound {F : ℝ × ℝ → ℝ}
        (hF : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) F) (hcF : HasCompactSupport F)
        {ε : ℝ} (hε : 0 < ε) (hz : ∀ a s, |s| < ε → F (a,s) = 0) :
        ∃ C : ℝ, 0 ≤ C ∧ ∀ {I : Set ℝ} {J : ℝ → ℝ} {P n : ℕ},
          IsOpen I → tsupport F ⊆ I ×ˢ univ → 0 < P → 0 < n →
          ∀ h : ℤ, ∀ L : ℝ, 0 < L → ∀ β : ℝ, (∀ a ∈ I, J a = L*a+β) →
          (∫ z, |foldCircleDensity (fineResidueKernel (passageBranchKernel I J F) P h n) z-
            foldCircleDensity (fun s => (P:ℝ)⁻¹*(∫ a, F (a,s))) z| ∂AddCircle.haarAddCircle) ≤ C/L := by
    …

    Mentions: OAI.ThreeTorus.foldCircleDensity, OAI.ThreeTorus.fineResidueKernel, OAI.ThreeTorus.passageBranchKernel

22. lemma OAI.ThreeTorus.exact_neutral_circle_spectral_estimate line 475

    Source documentation

    The broad slope is chosen after the cutoff weight and before the periodic jitter is fixed; the final passage integer is only subject to a lower bound. The displayed reference density is exactly the old cutoff stationary marginal, folded to the temporal circle and divided by the residue modulus.

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

23. theorem OAI.ThreeTorus.exists_integral_speed_separation line 590

    Source documentation

    One integral shift separates the speed ranges for all distinct integer angular indices in a finite list. It also keeps every range away from zero.

    theorem exists_integral_speed_separation {ι X : Type*} [Finite ι]
        [TopologicalSpace X] [CompactSpace X] (m : ι → ℤ) (φ : X → ℝ)
        (hm : ∀ i, m i ≠ 0) (hφ : Continuous φ) :
        ∃ c : ℕ, 0 < c ∧
          (∀ i x, (m i : ℝ) * ((c:ℝ) + φ x) ≠ 0) ∧
          (∀ i j x y, (m i : ℝ) * ((c:ℝ) + φ x) =
            (m j : ℝ) * ((c:ℝ) + φ y) → m i = m j) := by
    …

24. def OAI.ThreeTorus.stationaryImage line 633

    Source documentation

    A stationary image of an amplitude support. The pair records frequency and the unchanged slow coordinate.

    def stationaryImage (m : ℤ) (V : ℝ → ℝ) (K : Set (ℝ × UnitAddCircle)) :
        Set (ℝ × UnitAddCircle) :=
    …

25. lemma OAI.ThreeTorus.stationaryImage_compact line 637
26. lemma OAI.ThreeTorus.stationaryImage_disjoint_same line 643

    Source documentation

    For equal angular indices, branch injectivity preserves the exact gaps between disjoint coefficient supports.

    lemma stationaryImage_disjoint_same {m : ℤ} (hm : m ≠ 0) {V : ℝ → ℝ} {I : Set ℝ}
        (hV : InjOn V I) {K L : Set (ℝ × UnitAddCircle)}
        (hK : K ⊆ I ×ˢ univ) (hL : L ⊆ I ×ˢ univ) (hd : Disjoint K L) :
        Disjoint (stationaryImage m V K) (stationaryImage m V L) := by
    …

    Mentions: OAI.ThreeTorus.stationaryImage

27. lemma OAI.ThreeTorus.stationaryImage_disjoint_distinct line 656

    Source documentation

    Different angular indices are separated by their frequency ranges.

    lemma stationaryImage_disjoint_distinct {m n : ℤ} {V : ℝ → ℝ}
        {K L : Set (ℝ × UnitAddCircle)}
        (hsep : ∀ p ∈ K, ∀ q ∈ L, (m:ℝ)*V p.1 ≠ (n:ℝ)*V q.1) :
        Disjoint (stationaryImage m V K) (stationaryImage n V L) := by
    …

    Mentions: OAI.ThreeTorus.stationaryImage