OAI/Dynamics/ThreeTorus/Preparation.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThreeTorus.real_perturbation_nonzero_ae line 23

   Source documentation

   Apart from a Lebesgue null set of real parameters, a real perturbation has no zero where the target coefficient is nonzero, up to the original measure. This is the Fubini step in the manuscript, also for complex coefficients.

   lemma real_perturbation_nonzero_ae {X : Type*} [MeasurableSpace X]
       (μ : Measure X) [SFinite μ] {F H : X → ℂ}
       (hF : Measurable F) (hH : Measurable H) :
       ∀ᵐ t : ℝ, ∀ᵐ x ∂μ, F x + (t : ℂ) * H x = 0 → H x = 0 := by
   …

   Mentions: OAI.ThreeTorus.μ, OAI.ThreeTorus.H

2. lemma OAI.ThreeTorus.real_perturbation_family_ae line 49

   Source documentation

   The common real parameter avoids all the finite/countable list's bad fibers.

   lemma real_perturbation_family_ae {X ι : Type*} [MeasurableSpace X] [Countable ι]
       (μ : Measure X) [SFinite μ] {F H : ι → X → ℂ}
       (hF : ∀ i, Measurable (F i)) (hH : ∀ i, Measurable (H i)) :
       ∀ᵐ t : ℝ, ∀ i, ∀ᵐ x ∂μ, F i x + (t : ℂ) * H i x = 0 → H i x = 0 := by
   …

   Mentions: OAI.ThreeTorus.μ, OAI.ThreeTorus.H

3. lemma OAI.ThreeTorus.real_perturbation_zero_set_integral line 58

   Source documentation

   The exact weighted zero-set integral asserted in the paper.

   lemma real_perturbation_zero_set_integral {X : Type*} [MeasurableSpace X]
       (μ : Measure X) [SFinite μ] {F H : X → ℂ}
       (hF : Measurable F) (hH : Measurable H) :
       ∀ᵐ t : ℝ, ∫ x in {x | F x + (t : ℂ) * H x = 0}, ‖H x‖ ^ 2 ∂μ = 0 := by
   …

   Mentions: OAI.ThreeTorus.μ, OAI.ThreeTorus.H

4. lemma OAI.ThreeTorus.exists_small_real_perturbation line 72

   Source documentation

   The parameter may be chosen positive and smaller than any prescribed tolerance, simultaneously for a countable family of coefficient pairs.

   lemma exists_small_real_perturbation {X ι : Type*} [MeasurableSpace X] [Countable ι]
       (μ : Measure X) [SFinite μ] {F H : ι → X → ℂ}
       (hF : ∀ i, Measurable (F i)) (hH : ∀ i, Measurable (H i))
       {ε : ℝ} (hε : 0 < ε) :
       ∃ t : ℝ, 0 < t ∧ t < ε ∧
         ∀ i, ∀ᵐ x ∂μ, F i x + (t : ℂ) * H i x = 0 → H i x = 0 := by
   …

   Mentions: OAI.ThreeTorus.μ, OAI.ThreeTorus.H

5. def OAI.ThreeTorus.coefficientMeasure line 86

   Source documentation

   The weighted coefficient measure in the constant-ratio preparation.

   def coefficientMeasure {X : Type*} [MeasurableSpace X]
       (μ : Measure X) (F : X → ℂ) : Measure X :=
   …

   Mentions: OAI.ThreeTorus.μ

6. lemma OAI.ThreeTorus.ratio_mul_ae line 90
7. lemma OAI.ThreeTorus.ratio_memLp line 101

   Source documentation

   Ratios are genuinely square integrable for the weighted measure; no nonvanishing hypothesis on the source coefficient is imposed everywhere.

   lemma ratio_memLp {X : Type*} [MeasurableSpace X]
       {μ : Measure X} {F H : X → ℂ} (hF : Measurable F) (hH : Measurable H)
       (hH₂ : MemLp H 2 μ) (hzero : ∀ᵐ x ∂μ, F x = 0 → H x = 0) :
       MemLp (fun x => H x / F x) 2 (coefficientMeasure μ F) := by
   …

   Mentions: OAI.ThreeTorus.μ, OAI.ThreeTorus.H, OAI.ThreeTorus.coefficientMeasure

8. lemma OAI.ThreeTorus.ratio_integral_sq line 117

   Source documentation

   Exact weighted L² identity, as used before ratio truncation and rectangular approximation in the manuscript.

   lemma ratio_integral_sq {X : Type*} [MeasurableSpace X]
       {μ : Measure X} {F H : X → ℂ} (hF : Measurable F)
       (hzero : ∀ᵐ x ∂μ, F x = 0 → H x = 0) :
       (∫ x, ‖H x / F x‖ ^ 2 ∂coefficientMeasure μ F) = ∫ x, ‖H x‖ ^ 2 ∂μ := by
   …

   Mentions: OAI.ThreeTorus.μ, OAI.ThreeTorus.H, OAI.ThreeTorus.coefficientMeasure

9. lemma OAI.ThreeTorus.simple_compact_capture line 144
10. lemma OAI.ThreeTorus.disjoint_cutoffs_value line 183
11. theorem OAI.ThreeTorus.simple_smooth_disjoint_capture line 197

    Source documentation

    Smooth disjoint bump representation agrees with a prescribed simple function off a set of arbitrarily small measure. It also recovers the untagged constant one there. Zero simple values are retained as colors.

    theorem simple_smooth_disjoint_capture (ν : Measure (ℝ × UnitAddCircle)) [IsFiniteMeasure ν]
        [ν.InnerRegularCompactLTTop] (s : SimpleFunc (ℝ × UnitAddCircle) ℂ)
        {U : Set (ℝ × UnitAddCircle)} (hU : IsOpen U) (hν : ν Uᶜ = 0)
        {ε : ℝ≥0∞} (hε : ε ≠ 0) :
        ∃ χ : ↥s.range → ℝ × UnitAddCircle → ℝ,
          (∀ i, CylinderSmooth (χ i) ∧ HasCompactSupport (χ i) ∧ tsupport (χ i) ⊆ U ∧
            ∀ x, 0 ≤ χ i x ∧ χ i x ≤ 1) ∧
          Pairwise (fun i j => Disjoint (tsupport (χ i)) (tsupport (χ j))) ∧
          ∃ Z : Set (ℝ × UnitAddCircle), MeasurableSet Z ∧ ν Z < ε ∧
            ∀ x ∉ Z, (∑ i, χ i x) = 1 ∧ (∑ i, i.val * (χ i x:ℂ)) = s x := by
    …

    Mentions: OAI.ThreeTorus.CylinderSmooth

12. lemma OAI.ThreeTorus.exists_measure_bound_eLpNorm_lt line 242

    Source documentation

    A bounded error supported on a sufficiently small set has small L² norm. The bound is selected before the exceptional set/cutoffs are selected.

    lemma exists_measure_bound_eLpNorm_lt {X E : Type*} [MeasurableSpace X]
        [NormedAddCommGroup E] (μ : Measure X) {B : ℝ} (hB : 0 ≤ B)
        {ε : ℝ≥0∞} (hε : ε ≠ 0) :
        ∃ δ : ℝ≥0∞, 0 < δ ∧ ∀ (Z : Set X), MeasurableSet Z → μ Z < δ →
          ∀ f : X → E, AEStronglyMeasurable f μ →
            (∀ x, ‖f x‖ ≤ B) → (∀ x ∉ Z, f x = 0) → eLpNorm f 2 μ < ε := by
    …

    Mentions: OAI.ThreeTorus.μ

13. theorem OAI.ThreeTorus.weighted_smooth_disjoint_approx line 282

    Source documentation

    Weighted simultaneous approximation of the untagged vector and its measurable ratio. The finite constants are fixed before the interior trimming; zero constants are not discarded.

    theorem weighted_smooth_disjoint_approx (ν : Measure (ℝ × UnitAddCircle)) [IsFiniteMeasure ν]
        [ν.InnerRegularCompactLTTop] {R : ℝ × UnitAddCircle → ℂ} (hR : MemLp R 2 ν)
        {U : Set (ℝ × UnitAddCircle)} (hU : IsOpen U) (hν : ν Uᶜ = 0)
        {ε : ℝ≥0∞} (hε : ε ≠ 0) :
        ∃ s : SimpleFunc (ℝ × UnitAddCircle) ℂ,
        ∃ χ : ↥s.range → ℝ × UnitAddCircle → ℝ,
          (∀ i, CylinderSmooth (χ i) ∧ HasCompactSupport (χ i) ∧ tsupport (χ i) ⊆ U ∧
            ∀ x, 0 ≤ χ i x ∧ χ i x ≤ 1) ∧
          Pairwise (fun i j => Disjoint (tsupport (χ i)) (tsupport (χ j))) ∧
          eLpNorm (fun x => (1:ℂ) - ∑ i, (χ i x:ℂ)) 2 ν < ε ∧
          eLpNorm (fun x => R x - ∑ i, i.val * (χ i x:ℂ)) 2 ν < ε := by
    …

    Mentions: OAI.ThreeTorus.CylinderSmooth

14. lemma OAI.ThreeTorus.eLpNorm_coefficientMeasure line 363
15. lemma OAI.ThreeTorus.finite_coefficientMeasure line 380
16. theorem OAI.ThreeTorus.coefficient_smooth_disjoint_approx line 390

    Source documentation

    The literal coefficient errors after constant-ratio trimming, not just errors of the ratios in an auxiliary weighted space.

    theorem coefficient_smooth_disjoint_approx (μ : Measure (ℝ × UnitAddCircle))
        {F H : ℝ × UnitAddCircle → ℂ} (hFm : Measurable F) (hHm : Measurable H)
        (hF : MemLp F 2 μ) (hH : MemLp H 2 μ)
        (hzero : ∀ᵐ x ∂μ, F x = 0 → H x = 0)
        {U : Set (ℝ × UnitAddCircle)} (hU : IsOpen U)
        (hsupp : ∀ᵐ x ∂μ, x ∉ U → F x = 0) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
        ∃ s : SimpleFunc (ℝ × UnitAddCircle) ℂ,
        ∃ χ : ↥s.range → ℝ × UnitAddCircle → ℝ,
          (∀ i, CylinderSmooth (χ i) ∧ HasCompactSupport (χ i) ∧ tsupport (χ i) ⊆ U ∧
            ∀ x, 0 ≤ χ i x ∧ χ i x ≤ 1) ∧
          Pairwise (fun i j => Disjoint (tsupport (χ i)) (tsupport (χ j))) ∧
          eLpNorm (fun x => F x - ∑ i, (χ i x:ℂ)*F x) 2 μ < ε ∧
    …

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

17. def OAI.ThreeTorus.cylinderVolume line 443

    Source documentation

    Fundamental cylinder with the exact normalized slow-coordinate measure.

    def cylinderVolume (o : ℝ) : Measure (ℝ × UnitAddCircle) :=
    …

18. def OAI.ThreeTorus.cylinderToSlow line 446
19. def OAI.ThreeTorus.slowToCylinder line 448
20. lemma OAI.ThreeTorus.measurePreserving_cylinderToSlow line 451
21. lemma OAI.ThreeTorus.measurable_slowToCylinder line 458
22. lemma OAI.ThreeTorus.cylinderToSlow_slowToCylinder line 461
23. lemma OAI.ThreeTorus.slowToCylinder_cylinderToSlow line 465
24. lemma OAI.ThreeTorus.measurePreserving_slowToCylinder line 477
25. instance OAI.ThreeTorus.(instance at line 484) line 484
26. lemma OAI.ThreeTorus.eLpNorm_cylinder_pull line 488
27. lemma OAI.ThreeTorus.eLpNorm_slow_pull line 493
28. def OAI.ThreeTorus.multiTrigPolynomial line 515
29. lemma OAI.ThreeTorus.multiTrigPolynomial_apply line 518
30. lemma OAI.ThreeTorus.mFourier_smooth_lift line 522
31. lemma OAI.ThreeTorus.multiTrigPolynomial_smooth_lift line 531
32. theorem OAI.ThreeTorus.exists_L2_multiTrig line 539

    Source documentation

    The exact existing multivariate Fourier basis supplies smooth finite polynomials in the FULL torus space, not just a cyclic subspace.

    theorem exists_L2_multiTrig {f : UnitAddTorus d → ℂ} (hf : MemLp f 2 volume)
        {ε : ℝ} (hε : 0 < ε) :
        ∃ c : (d → ℤ) →₀ ℂ,
          eLpNorm (fun x => f x-multiTrigPolynomial c x) 2 volume < ENNReal.ofReal ε := by
    …

    Mentions: OAI.ThreeTorus.multiTrigPolynomial

33. lemma OAI.ThreeTorus.exists_uniform_multiTrig line 563
34. def OAI.ThreeTorus.slowPair line 594
35. lemma OAI.ThreeTorus.slowPair_symm_apply line 597
36. lemma OAI.ThreeTorus.continuous_slowPair_symm line 599
37. lemma OAI.ThreeTorus.measurePreserving_slowPair line 606
38. lemma OAI.ThreeTorus.exists_smooth_slow_approx line 611

    Source documentation

    Arbitrary actual L² coefficients admit smooth periodic approximation in both slow variables. Density is in the full two-torus L² space.

    lemma exists_smooth_slow_approx {f : UnitAddCircle × UnitAddCircle → ℂ}
        (hf : MemLp f 2 slowVolume) {ε : ℝ} (hε : 0 < ε) :
        ∃ g : UnitAddCircle × UnitAddCircle → ℂ, Continuous g ∧
          ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (fun p : ℝ × ℝ => g (p.1,p.2)) ∧
          eLpNorm (fun p => f p-g p) 2 slowVolume < ENNReal.ofReal ε := by
    …

    Mentions: OAI.ThreeTorus.slowVolume

39. lemma OAI.ThreeTorus.circleRep_mem line 646
40. lemma OAI.ThreeTorus.cylinderTorusCutoff_rep line 649
41. lemma OAI.ThreeTorus.cylinderTorusCutoff_bounds line 655
42. lemma OAI.ThreeTorus.cylinderTorusCutoff_fixes line 662
43. lemma OAI.ThreeTorus.exists_supported_slow_approx line 678

    Source documentation

    The same smooth compact cutoff preserves the supported old coefficient, and smooths without any extra approximation loss.

    lemma exists_supported_slow_approx {f : UnitAddCircle × UnitAddCircle → ℂ}
        (hf : MemLp f 2 slowVolume) {χ : ℝ × UnitAddCircle → ℝ} {o l u : ℝ}
        (hχs : CylinderSmooth χ) (hχc : HasCompactSupport χ)
        (hχsupp : support χ ⊆ Ioo o (o+1) ×ˢ univ)
        (hχb : ∀ p, 0 ≤ χ p ∧ χ p ≤ 1) (hol : o < l) (huo : u < o+1)
        (hχ1 : ∀ p ∈ Icc l u ×ˢ univ, χ p = 1)
        (hfs : support f ⊆ ((fun x : ℝ => (x:UnitAddCircle)) '' Icc l u) ×ˢ univ)
        {ε : ℝ} (hε : 0 < ε) :
        ∃ g : UnitAddCircle × UnitAddCircle → ℂ, Continuous g ∧
          ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (fun p : ℝ × ℝ => g (p.1,p.2)) ∧
          eLpNorm (fun p => f p-(cylinderTorusCutoff χ p:ℂ)*g p) 2 slowVolume < ENNReal.ofReal ε := by
    …

    Mentions: OAI.ThreeTorus.slowVolume, OAI.ThreeTorus.CylinderSmooth, OAI.ThreeTorus.cylinderTorusCutoff

44. lemma OAI.ThreeTorus.cylinder_mem_open_ae line 717
45. theorem OAI.ThreeTorus.torus_coefficient_smooth_disjoint_approx line 730

    Source documentation

    Actual torus coefficient version of weighted ratio approximation. The cutoffs are compact on the cylinder, but both errors are in normalized torus L². No mass is dropped where the finite tag is zero.

    theorem torus_coefficient_smooth_disjoint_approx (o : ℝ)
        {F H : UnitAddCircle × UnitAddCircle → ℂ} (hFm : Measurable F) (hHm : Measurable H)
        (hF : MemLp F 2 slowVolume) (hH : MemLp H 2 slowVolume)
        (hzero : ∀ᵐ x ∂slowVolume, F x=0 → H x=0)
        {ε : ℝ≥0∞} (hε : ε ≠ 0) :
        ∃ s : SimpleFunc (ℝ × UnitAddCircle) ℂ,
        ∃ χ : ↥s.range → ℝ × UnitAddCircle → ℝ,
          (∀ i, CylinderSmooth (χ i) ∧ HasCompactSupport (χ i) ∧
            tsupport (χ i) ⊆ Ioo o (o+1) ×ˢ univ ∧ ∀ x, 0 ≤ χ i x ∧ χ i x ≤ 1) ∧
          Pairwise (fun i j => Disjoint (tsupport (χ i)) (tsupport (χ j))) ∧
          eLpNorm (fun x => F x - ∑ i, (cylinderTorusCutoff (χ i) x:ℂ)*F x) 2 slowVolume < ε ∧
          eLpNorm (fun x => H x - ∑ i, i.val*((cylinderTorusCutoff (χ i) x:ℂ)*F x)) 2 slowVolume < ε := by
    …

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

46. lemma OAI.ThreeTorus.vector_reindex_equiv line 781
47. lemma OAI.ThreeTorus.tagged_vector_reindex_equiv line 787
48. theorem OAI.ThreeTorus.exists_reflected_ratio_packets line 797

    Source documentation

    Source05 constant-ratio preparation, including all zero-tag pieces. The finite constant tags and compact smooth supports are chosen on positive modes, then reflected literally. No weighted null set is divided by.

    theorem exists_reflected_ratio_packets {ι : Type} [Fintype ι]
        (F : PassagePackets ι) (hi : Injective F.m)
        {τ : ι → ι} (hr : F.Reflection τ)
        (H : ι → UnitAddCircle × UnitAddCircle → ℂ)
        (hHm : ∀ i, Measurable (H i)) (hHl : ∀ i, MemLp (H i) 2 slowVolume)
        (hHr : ∀ i p, H (τ i) p=conj (H i p))
        (hzero : ∀ i, ∀ᵐ p ∂slowVolume, F.A i p=0 → H i p=0)
        {δ ε : ℝ} (hg : F.GoodArc δ) (hε : 0 < ε) :
        ∃ n : ℕ, ∃ G : PassagePackets (Fin n), ∃ σ : Fin n → Fin n, ∃ b : Fin n → ℂ,
          G.V=F.V ∧ G.GoodArc δ ∧ Involutive σ ∧ G.Reflection σ ∧
          (∀ i, b (σ i)=conj (b i)) ∧
          (∀ i j, i ≠ j → G.m i=G.m j → Disjoint (G.cylinderCore i) (G.cylinderCore j)) ∧
    …

    Mentions: OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.H, OAI.ThreeTorus.slowVolume

49. lemma OAI.ThreeTorus.physicalDist_add_smul line 881
50. lemma OAI.ThreeTorus.PassagePackets.append_weighted_vector line 894
51. lemma OAI.ThreeTorus.PassagePackets.modeSum_add_amplitude line 903
52. theorem OAI.ThreeTorus.exists_ratio_packets_for_pair line 919

    Source documentation

    Two actual real smooth packet vectors in a common good-arc twist admit simultaneous constant-tag clipping. Repeated modes are honestly regrouped; zero pieces of either vector are retained before the real null-set perturbation.

    theorem exists_ratio_packets_for_pair {ι κ : Type} [Fintype ι] [Fintype κ]
        (F : PassagePackets ι) (H : PassagePackets κ) {δ : ℝ}
        (hδ : 0 ≤ δ) (hgF : F.GoodArc δ) (hgH : H.GoodArc δ) (hV : H.V=F.V)
        (τ : ι → ι) (σ : κ → κ) (hτ : Involutive τ) (hσ : Involutive σ)
        (hrF : F.Reflection τ) (hrH : H.Reflection σ)
        {ε : ℝ} (hε : 0 < ε) :
        ∃ n : ℕ, ∃ G : PassagePackets (Fin n), ∃ ρ : Fin n → Fin n, ∃ b : Fin n → ℂ,
          G.V=F.V ∧ G.GoodArc δ ∧ Involutive ρ ∧ G.Reflection ρ ∧
          (∀ i, b (ρ i)=conj (b i)) ∧
          (∀ i j, i ≠ j → G.m i=G.m j → Disjoint (G.cylinderCore i) (G.cylinderCore j)) ∧
          physicalDist (finitePacketVector F.m F.A) (finitePacketVector G.m G.A) < ε ∧
          physicalDist (finitePacketVector H.m H.A) (fun x => ∑ i, b i*packet (G.m i) (G.A i) x) < ε := by
    …

    Mentions: OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.H, OAI.ThreeTorus.physicalDist, OAI.ThreeTorus.finitePacketVector, OAI.ThreeTorus.packet

53. structure OAI.ThreeTorus.RealPacketFamily line 1006

    Source documentation

    A finite literal real smooth packet list. Repeated frequencies are permitted; no orthogonality is part of this bookkeeping structure.

    structure RealPacketFamily where
    …

54. def OAI.ThreeTorus.RealPacketFamily.vector line 1016
55. def OAI.ThreeTorus.RealPacketFamily.density line 1017
56. lemma OAI.ThreeTorus.RealPacketFamily.continuous_vector line 1018
57. lemma OAI.ThreeTorus.RealPacketFamily.vector_memLp line 1020
58. lemma OAI.ThreeTorus.RealPacketFamily.vector_real line 1022
59. lemma OAI.ThreeTorus.RealPacketFamily.vector_centered line 1024
60. lemma OAI.ThreeTorus.RealPacketFamily.density_nonneg line 1027
61. lemma OAI.ThreeTorus.RealPacketFamily.density_measurable line 1029
62. lemma OAI.ThreeTorus.RealPacketFamily.density_integrable line 1031
63. def OAI.ThreeTorus.RealPacketFamily.append line 1034
64. lemma OAI.ThreeTorus.RealPacketFamily.append_vector line 1045
65. lemma OAI.ThreeTorus.RealPacketFamily.density_energy line 1053
66. theorem OAI.ThreeTorus.exists_neutral_families line 1078
67. lemma OAI.ThreeTorus.physicalDist_continuous_comp line 1096
68. lemma OAI.ThreeTorus.physicalDist_add_right line 1102
69. lemma OAI.ThreeTorus.densityDist_triangle line 1107
70. lemma OAI.ThreeTorus.multiTrigPolynomial_add line 1132
71. lemma OAI.ThreeTorus.multiTrigPolynomial_smul line 1137
72. lemma OAI.ThreeTorus.multiTrigPolynomial_single line 1143
73. def OAI.ThreeTorus.conjugateCoefficients line 1148
74. lemma OAI.ThreeTorus.conjugateCoefficients_apply line 1152
75. lemma OAI.ThreeTorus.multiTrigPolynomial_conjugate line 1158
76. lemma OAI.ThreeTorus.integral_mFourier line 1166
77. lemma OAI.ThreeTorus.integral_multiTrigPolynomial line 1172
78. theorem OAI.ThreeTorus.exists_real_centered_uniform_multiTrig line 1186

    Source documentation

    A finite FULL-torus polynomial can be made exactly real and centered, with reflected coefficients, without changing the density statement.

    theorem exists_real_centered_uniform_multiTrig {h : UnitAddTorus d → ℂ}
        (hh : Continuous h) (hr : ∀ x, conj (h x) = h x)
        (hc : ∫ x, h x = 0) {ε : ℝ} (hε : 0 < ε) :
        ∃ c : (d → ℤ) →₀ ℂ, c 0 = 0 ∧ (∀ k, c (-k)=conj (c k)) ∧
          ∀ x, ‖h x-multiTrigPolynomial c x‖ < ε := by
    …

    Mentions: OAI.ThreeTorus.multiTrigPolynomial

79. def OAI.ThreeTorus.toTriple line 1252

    Source documentation

    The coordinate convention used by the analytic packet calculations.

    def toTriple : Torus ≃ᵐ TripleTorus :=
    …

    Mentions: OAI.ThreeTorus.Torus, OAI.ThreeTorus.TripleTorus

80. lemma OAI.ThreeTorus.toTriple_apply line 1257
81. lemma OAI.ThreeTorus.toTriple_symm_apply line 1259
82. lemma OAI.ThreeTorus.measurePreserving_toTriple line 1264
83. lemma OAI.ThreeTorus.integral_sq_sub_mean line 1282

    Source documentation

    Removing a fiber mean is an orthogonal projection, with constant ONE. This is the estimate preserving the source good-arc sqrt(beta) loss.

    lemma integral_sq_sub_mean {X : Type*} [MeasurableSpace X] {μ : Measure X}
        [IsProbabilityMeasure μ] {f : X → ℂ} (hf : MemLp f 2 μ) :
        (∫ x, ‖f x-∫ y, f y ∂μ‖^2 ∂μ) =
          (∫ x, ‖f x‖^2 ∂μ)-‖∫ y, f y ∂μ‖^2 := by
    …

    Mentions: OAI.ThreeTorus.μ

84. lemma OAI.ThreeTorus.integral_sq_sub_mean_le line 1302
85. abbrev OAI.ThreeTorus.TensorIndex line 1323
86. def OAI.ThreeTorus.tensorCharacter line 1325
87. lemma OAI.ThreeTorus.mFourier_toTriple line 1328
88. def OAI.ThreeTorus.tensorPolynomial line 1335
89. lemma OAI.ThreeTorus.tensorPolynomial_eq line 1338
90. lemma OAI.ThreeTorus.continuous_toTriple line 1342
91. lemma OAI.ThreeTorus.continuous_toTriple_symm line 1346
92. lemma OAI.ThreeTorus.tensorCharacter_continuous line 1350
93. lemma OAI.ThreeTorus.tensorPolynomial_continuous line 1354
94. lemma OAI.ThreeTorus.exists_real_centered_tensor line 1358
95. def OAI.ThreeTorus.tensorAngular line 1372

    Source documentation

    Angular split, first slow split, and the final centered slow average.

    def tensorAngular (c : TensorIndex →₀ ℂ) : TensorIndex →₀ ℂ :=
    …

    Mentions: OAI.ThreeTorus.TensorIndex

96. def OAI.ThreeTorus.tensorMiddle line 1374
97. def OAI.ThreeTorus.tensorLast line 1376
98. lemma OAI.ThreeTorus.tensor_split line 1379
99. lemma OAI.ThreeTorus.tensorLast_nonzero line 1386
100. def OAI.ThreeTorus.cutoffPackets line 1410

     Source documentation

     Build literal smooth passage input coefficients from compact smooth cylinder cutoffs and smooth periodic two-torus coefficients.

     def cutoffPackets {ι : Type*} (m : ι → ℤ) (hm : ∀ i, m i ≠ 0)
         (C : ι → UnitAddCircle × UnitAddCircle → ℂ)
         (hCc : ∀ i, Continuous (C i))
         (hCs : ∀ i, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (fun p : ℝ × ℝ => C i (p.1,p.2)))
         (χ : ι → ℝ × UnitAddCircle → ℝ) (hχs : ∀ i, CylinderSmooth (χ i))
         (hχc : ∀ i, HasCompactSupport (χ i))
         (o l u R : ℝ) (hχo : ∀ i, support (χ i) ⊆ Ioo o (o+1) ×ˢ univ)
         (hχI : ∀ i, support (χ i) ⊆ Ioc l u ×ˢ univ)
         (hlo : o ≤ l) (huo : u ≤ o+1) (hlu : l ≤ u) (hR : 0 < R)
         (V : ℝ → ℝ) (hVp : Periodic V 1)
         (hVs : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V)
         (hVd : ∀ x ∈ Icc (l-2*R) (u+2*R), 0 < deriv V x) : PassagePackets ι where
     …

     Mentions: OAI.ThreeTorus.CylinderSmooth, OAI.ThreeTorus.PassagePackets

101. lemma OAI.ThreeTorus.NeutralStep.core_eq line 1480
102. lemma OAI.ThreeTorus.NeutralStep.cores_disjoint line 1488
103. theorem OAI.ThreeTorus.NeutralStep.second_cutoffs line 1498

     Source documentation

     Reflection-compatible scalar cutoffs on the actual first output. Their supports are disjoint on the frequency line, not merely on the cylinder.

     theorem second_cutoffs [Fintype ι]
         (hd : Pairwise (fun i j => Disjoint (tsupport (s.χ i).uncurry) (tsupport (s.χ j).uncurry)))
         {τ : PassageOutputIndex s.S → PassageOutputIndex s.S}
         (hτ : Involutive τ) (hr : s.final.Reflection τ) :
         ∃ c : ℕ, 0 < c ∧ (∀ x : ℝ, (c:ℝ)+s.final.V x ≠ 0) ∧
           ∃ ξ : PassageOutputIndex s.S → ℝ → ℝ,
             (∀ i, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (ξ i) ∧ HasCompactSupport (ξ i) ∧
               ξ i 0 = 0 ∧ (∀ x, 0 ≤ ξ i x ∧ ξ i x ≤ 1) ∧
               ∀ (C : Set ℝ) a x, stationaryWeight C
                 (fun t => (s.final.m i:ℝ)*((c:ℝ)+s.final.V t)) (s.final.A₀ i a) x ≠ 0 → ξ i x = 1) ∧
             Pairwise (fun i j => Disjoint (tsupport (ξ i)) (tsupport (ξ j))) ∧
             ∀ i x, ξ (τ i) x = ξ i (-x) := by
     …

     Mentions: OAI.ThreeTorus.PassageOutputIndex, OAI.ThreeTorus.stationaryWeight

104. lemma OAI.ThreeTorus.scalar_cylinder_compact line 1563
105. theorem OAI.ThreeTorus.exists_two_neutral_separations line 1572

     Source documentation

     Neither intermediate modes nor intermediate coefficients are replaced by an independent spectral model. All estimates concern the two actual charts.

     theorem exists_two_neutral_separations {ι : Type} [Fintype ι]
         (F : PassagePackets ι)
         (hd : ∀ i j, i ≠ j → F.m i = F.m j → Disjoint (F.cylinderCore i) (F.cylinderCore j))
         (τ : ι → ι) (hτ : Involutive τ) (hr : F.Reflection τ)
         (Q : PhysicalJetData) (frame : PhysicalFrame)
         {ε κ ζ : ℝ} (hε : 0 < ε) (hκ : 0 < κ) (hζ : 0 < ζ) :
         ∃ s : NeutralStep F, ∃ t : NeutralStep s.final,
           Injective t.final.m ∧ t.δ < κ ∧
           (∃ τT : PassageOutputIndex t.S → PassageOutputIndex t.S,
             Involutive τT ∧ t.final.Reflection τT ∧ ∀ i, (τT i).1.1 = τ i.1.1) ∧
           Q.Close ζ frame F.V (t.nextFrame (s.nextFrame frame)) t.final.V ∧
           ∀ i, physicalError (packet (F.m i) (F.A i))
     …

     Mentions: OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.PhysicalJetData, OAI.ThreeTorus.PhysicalFrame, OAI.ThreeTorus.NeutralStep, OAI.ThreeTorus.PassageOutputIndex, OAI.ThreeTorus.physicalError, OAI.ThreeTorus.packet