OAI/Dynamics/ThreeTorus/FlatPackets.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

Flat support, finite packet L2 estimates, neutral selection, density invariance, and finite spectral whitening.

  1. lemma OAI.ThreeTorus.memLp_packet line 17

    Source documentation

    Packets of arbitrary L² coefficients have the same norm as their coefficients.

    lemma memLp_packet {A : UnitAddCircle × UnitAddCircle → ℂ}
    (hA : MemLp A 2 slowVolume) (m : ℤ) : MemLp (packet m A) 2 tripleVolume := by
…

    Mentions: OAI.ThreeTorus.slowVolume, OAI.ThreeTorus.packet, OAI.ThreeTorus.tripleVolume

  2. lemma OAI.ThreeTorus.integral_packet_pair_L2 line 27
  3. lemma OAI.ThreeTorus.memLp_frequency_mul line 48
  4. lemma OAI.ThreeTorus.packet_correlation_L2 line 59

    Source documentation

    Exact correlation formula, requiring no smoothness of the coefficients.

    lemma packet_correlation_L2 {A : UnitAddCircle × UnitAddCircle → ℂ}
    (hA : MemLp A 2 slowVolume) {φ : UnitAddCircle → UnitAddCircle} (hφ : Measurable φ)
    (m n : ℤ) :
    (∫ x : TripleTorus, starRingEnd ℂ (packet m A x)*
      packet m A (twistIter φ n x) ∂tripleVolume) =
    ∫ ua : UnitAddCircle × UnitAddCircle,
      fourier n (m • φ ua.1)*(‖A ua‖^2 : ℝ) ∂slowVolume := by
…

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

  5. lemma OAI.ThreeTorus.packet_spectral_moment_L2 line 84

    Source documentation

    Exact pushforward measure even for the endpoint-discontinuous flat vector.

    lemma packet_spectral_moment_L2 {φ : UnitAddCircle → UnitAddCircle} (hφ : Measurable φ)
    {A : UnitAddCircle × UnitAddCircle → ℂ} (hAm : Measurable A)
    (hA : MemLp A 2 slowVolume) (m n : ℤ) :
    (∫ z, fourier n z ∂packetSpectralMeasure φ m A) =
      ∫ x : TripleTorus, starRingEnd ℂ (packet m A x)*
        packet m A (twistIter φ n x) ∂tripleVolume := by
…

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

  6. lemma OAI.ThreeTorus.packet_integral_zero line 101
  7. lemma OAI.ThreeTorus.map_jacobian_real line 115
  8. lemma OAI.ThreeTorus.flat_branch_mod_one line 124
  9. def OAI.ThreeTorus.circleRep line 142

    Source documentation

    The representative in the old good-arc coordinate chart.

    def circleRep (o : ℝ) (z : UnitAddCircle) : ℝ :=
…
  10. lemma OAI.ThreeTorus.measurable_circleRep line 145
  11. lemma OAI.ThreeTorus.circleRep_coe line 148
  12. lemma OAI.ThreeTorus.coe_circleRep line 152
  13. lemma OAI.ThreeTorus.circle_weight_lift line 156
  14. lemma OAI.ThreeTorus.flat_circle_branch line 178

    Source documentation

    The branch Jacobian realizes Haar measure for any circle map agreeing with that lifted frequency on the chosen interval.

    lemma flat_circle_branch {f D : ℝ → ℝ} {l u o : ℝ}
    {ζ : UnitAddCircle → UnitAddCircle}
    (hlu : l ≤ u) (hfm : Measurable f) (hDm : Measurable D)
    (hD : ∀ x ∈ Icc l u, HasDerivWithinAt f (D x) (Icc l u) x)
    (hmono : StrictMonoOn f (Icc l u)) (hperiod : f u = f l+1)
    (hi : Icc l u ⊆ Ioc o (o+1)) (hζ : Measurable ζ)
    (hζf : ∀ x ∈ Icc l u, ζ (x : UnitAddCircle) = (f x : UnitAddCircle)) :
    (AddCircle.haarAddCircle.withDensity
      (((Icc l u).indicator (fun x => ENNReal.ofReal |D x|)) ∘ circleRep o)).map ζ =
      AddCircle.haarAddCircle := by
…

    Mentions: OAI.ThreeTorus.circleRep

  15. def OAI.ThreeTorus.flatAmplitude line 214

    Source documentation

    The manuscript's endpoint-discontinuous coefficient.

    def flatAmplitude (o l u : ℝ) (D : ℝ → ℝ) (z : UnitAddCircle) : ℂ :=
…
  16. lemma OAI.ThreeTorus.measurable_flatAmplitude line 217
  17. lemma OAI.ThreeTorus.flatAmplitude_energy line 223
  18. lemma OAI.ThreeTorus.flatAmplitude_pushforward line 238
  19. lemma OAI.ThreeTorus.memLp_of_energy_map line 254

    Source documentation

    Finite total pushed energy implies L² membership, even without boundedness.

    lemma memLp_of_energy_map {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
    {μ : Measure X} {ν : Measure Y} [IsFiniteMeasure ν]
    {F : X → ℂ} {ζ : X → Y} (hF : Measurable F) (hζ : Measurable ζ)
    (he : (μ.withDensity (fun x => ENNReal.ofReal (‖F x‖^2))).map ζ = ν) :
    MemLp F 2 μ := by
…

    Mentions: OAI.ThreeTorus.μ

  20. lemma OAI.ThreeTorus.frequency_energy_neg line 270

    Source documentation

    Haar is invariant under reversing the additive spectral variable.

    lemma frequency_energy_neg {A : UnitAddCircle → ℂ} {ζ : UnitAddCircle → UnitAddCircle}
    (hζ : Measurable ζ) {c : ℝ≥0∞}
    (hpush : (AddCircle.haarAddCircle.withDensity
      (fun z => ENNReal.ofReal (‖A z‖^2))).map ζ = c • AddCircle.haarAddCircle) :
    (AddCircle.haarAddCircle.withDensity (fun z => ENNReal.ofReal (‖A z‖^2))).map
      (fun z => -(ζ z)) = c • AddCircle.haarAddCircle := by
…
  21. lemma OAI.ThreeTorus.packetSpectrum_first_coeff line 281
  22. def OAI.ThreeTorus.realPacketPair line 295

    Source documentation

    A pair of opposite angular modes with real coefficient.

    def realPacketPair (m : ℤ) (A : UnitAddCircle × UnitAddCircle → ℂ) (x : TripleTorus) : ℂ :=
…

    Mentions: OAI.ThreeTorus.TripleTorus

  23. lemma OAI.ThreeTorus.realPacketPair_real line 298
  24. lemma OAI.ThreeTorus.memLp_realPacketPair line 306
  25. lemma OAI.ThreeTorus.realPacketPair_integral_zero line 310
  26. lemma OAI.ThreeTorus.packet_twist_memLp line 318
  27. lemma OAI.ThreeTorus.packet_cross_correlation line 329
  28. lemma OAI.ThreeTorus.realPacketPair_correlation line 344
  29. lemma OAI.ThreeTorus.integral_fourier_haar line 364
  30. lemma OAI.ThreeTorus.realPacketPair_flat line 370
  31. lemma OAI.ThreeTorus.flatAmplitude_support line 385
  32. lemma OAI.ThreeTorus.flat_vector_of_branch line 397

    Source documentation

    The exact real centered two-mode flat vector on any branch of length one in the additive spectral variable. No coefficient smoothness is assumed.

    lemma flat_vector_of_branch {f D : ℝ → ℝ} {l u o : ℝ}
    {φ : UnitAddCircle → UnitAddCircle} {m : ℤ}
    (hm : m ≠ 0) (hlu : l ≤ u) (hfm : Measurable f) (hDm : Measurable D)
    (hD : ∀ x ∈ Icc l u, HasDerivWithinAt f (D x) (Icc l u) x)
    (hmono : StrictMonoOn f (Icc l u)) (hperiod : f u = f l+1)
    (hi : Icc l u ⊆ Ioc o (o+1)) (hφ : Measurable φ)
    (hφf : ∀ x ∈ Icc l u, m • φ (x : UnitAddCircle) = (f x : UnitAddCircle)) :
    let A := fun ua : UnitAddCircle × UnitAddCircle => flatAmplitude o l u D ua.1
…

    Mentions: OAI.ThreeTorus.flatAmplitude

  33. lemma OAI.ThreeTorus.exists_integer_period_subinterval line 437

    Source documentation

    Increasing on a nontrivial compact interval suffices to cover one period after multiplication by a positive integer, without changing its left endpoint.

    lemma exists_integer_period_subinterval {ψ : ℝ → ℝ} {l u : ℝ}
    (hlu : l < u) (hc : ContinuousOn ψ (Icc l u))
    (hmono : StrictMonoOn ψ (Icc l u)) :
    ∃ m : ℕ, 0 < m ∧ ∃ t ∈ Icc l u, l < t ∧ (m:ℝ)*(ψ t-ψ l) = 1 := by
…
  34. lemma OAI.ThreeTorus.exists_flat_vector_on_interval line 465

    Source documentation

    The full flat-vector construction on every increasing good-arc interval. The coefficient is literally the indicator times the square root Jacobian in the manuscript, and its support is in a compact subinterval of the good arc.

    lemma exists_flat_vector_on_interval {φ : UnitAddCircle → ℝ} {D : ℝ → ℝ}
    {l u o : ℝ} (hφ : Measurable φ) (hDm : Measurable D) (hlu : l < u)
    (hD : ∀ x ∈ Icc l u, HasDerivWithinAt
      (fun y : ℝ => φ (y : UnitAddCircle)) (D x) (Icc l u) x)
    (hmono : StrictMonoOn (fun y : ℝ => φ (y : UnitAddCircle)) (Icc l u))
    (hi : Icc l u ⊆ Ioc o (o+1)) :
    ∃ m : ℕ, 0 < m ∧ ∃ t ∈ Icc l u, l < t ∧
      let A := fun ua : UnitAddCircle × UnitAddCircle =>
…
  35. abbrev OAI.ThreeTorus.coefficientVolume line 521
  36. def OAI.ThreeTorus.finitePacketVector line 524
  37. def OAI.ThreeTorus.coefficientFrequency line 527
  38. lemma OAI.ThreeTorus.measurable_coefficientFrequency line 530
  39. lemma OAI.ThreeTorus.memLp_finitePacketVector line 535
  40. lemma OAI.ThreeTorus.finitePacketVector_sub line 540
  41. lemma OAI.ThreeTorus.finitePacket_inner line 547
  42. lemma OAI.ThreeTorus.finitePacket_energy line 562
  43. lemma OAI.ThreeTorus.integrable_coefficient_normsq line 570
  44. lemma OAI.ThreeTorus.coefficient_integral_normsq line 578
  45. lemma OAI.ThreeTorus.coefficient_memLp line 584
  46. lemma OAI.ThreeTorus.physicalDist_eLpNorm line 603
  47. lemma OAI.ThreeTorus.eLpNorm_packet line 609
  48. lemma OAI.ThreeTorus.physicalDist_packet line 621
  49. lemma OAI.ThreeTorus.physicalDist_packet_lt line 631
  50. lemma OAI.ThreeTorus.physicalDist_add_le line 639
  51. lemma OAI.ThreeTorus.physicalDist_small_sum line 650
  52. def OAI.ThreeTorus.NeutralStep.reindex line 685

    Source documentation

    Restrict a simultaneously transported finite family to a chosen root list. This is the SAME physical passage, not another existence choice.

    def reindex (r : κ → ι) : NeutralStep (F.reindex r) where
…

    Mentions: OAI.ThreeTorus.NeutralStep

  53. lemma OAI.ThreeTorus.NeutralStep.reindex_chart line 707
  54. lemma OAI.ThreeTorus.NeutralStep.reindex_nextFrame line 708
  55. lemma OAI.ThreeTorus.NeutralStep.reindex_outputVector line 711
  56. lemma OAI.ThreeTorus.NeutralStep.reindex_outputDensity line 716
  57. lemma OAI.ThreeTorus.NeutralStep.reindex_final_injective line 721
  58. lemma OAI.ThreeTorus.NeutralStep.finitePacketVector_output line 729

    Source documentation

    Exact vector regrouping of the retained coefficients over their old roots.

    lemma finitePacketVector_output [Fintype ι] :
    finitePacketVector s.final.m s.final.A = fun x => ∑ i, outputVector s.final i x := by
…

    Mentions: OAI.ThreeTorus.finitePacketVector, OAI.ThreeTorus.outputVector

  59. lemma OAI.ThreeTorus.NeutralStep.physicalDist_total line 734
  60. theorem OAI.ThreeTorus.exists_grouped_neutral line 771

    Source documentation

    A simultaneous neutral passage with repeated modes. Distinct old modes have disjoint scalar retained sets, and equal modes share the same cutoff.

    theorem exists_grouped_neutral {ι : Type*} [Fintype ι]
    (F : PassagePackets ι) (τ : ι → ι) (hτ : Involutive τ) (hr : F.Reflection τ)
    (Q : PhysicalJetData) (frame : PhysicalFrame)
    {ε κ ζ : ℝ} (hε : 0 < ε) (hκ : 0 < κ) (hζ : 0 < ζ) :
    ∃ s : NeutralStep F, s.δ < κ ∧
      Q.Close ζ frame F.V (s.nextFrame frame) s.final.V ∧
      (∀ i j, F.m i ≠ F.m j → Disjoint (s.S i) (s.S j)) ∧
      (∀ i x a, s.χ (τ i) x a=s.χ i (-x) a) ∧
      (∃ σ, Involutive σ ∧ s.final.Reflection σ ∧ ∀ i, (σ i).1=τ i.1) ∧
      ∀ i, physicalError (packet (F.m i) (F.A i))
        (outputVector s.final i ∘ s.chart) < ε ∧
        (∫ z, |outputDensity s.final i z-F.marginalDensity i z| ∂phaseHaar) < ε := by
…

    Mentions: OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.PhysicalJetData, OAI.ThreeTorus.PhysicalFrame, OAI.ThreeTorus.NeutralStep, OAI.ThreeTorus.physicalError, OAI.ThreeTorus.packet, OAI.ThreeTorus.outputVector, OAI.ThreeTorus.outputDensity, OAI.ThreeTorus.phaseHaar

  61. lemma OAI.ThreeTorus.PassagePackets.marginalDensity_congr line 814
  62. lemma OAI.ThreeTorus.PassagePackets.marginalDensity_reindex line 832
  63. lemma OAI.ThreeTorus.PassagePackets.append_marginalDensity_left line 835
  64. lemma OAI.ThreeTorus.integral_abs_sum_sub_le_of_integrable line 851
  65. lemma OAI.ThreeTorus.NeutralStep.density_total line 867
  66. theorem OAI.ThreeTorus.exists_neutral_pair line 890

    Source documentation

    Simultaneous transport of two real lists with the SAME physical passage. The first list retains injective angular indices; no cross-list orthogonality or disjointness is assumed.

    theorem exists_neutral_pair {ι κ : Type*} [Fintype ι] [Fintype κ]
    (F : PassagePackets ι) (H : PassagePackets κ) (hmi : Injective F.m)
    {δ : ℝ} (hδ : 0 ≤ δ) (hgF : F.GoodArc δ) (hgH : H.GoodArc δ) (hV : H.V=F.V)
    (τ : ι → ι) (σ : κ → κ) (hτ : Involutive τ) (hσ : Involutive σ)
    (hrF : F.Reflection τ) (hrH : H.Reflection σ)
    (Q : PhysicalJetData) (frame : PhysicalFrame)
    {ε η ζ : ℝ} (hε : 0 < ε) (hη : 0 < η) (hζ : 0 < ζ) :
    ∃ s : NeutralStep (F.append H hδ hgF hgH hV),
      s.δ < η ∧ Q.Close ζ frame F.V (s.nextFrame frame) s.final.V ∧
      Injective (s.reindex Sum.inl).final.m ∧
      (∃ τ', Involutive τ' ∧ (s.reindex Sum.inl).final.Reflection τ') ∧
      (∃ σ', Involutive σ' ∧ (s.reindex Sum.inr).final.Reflection σ') ∧
…

    Mentions: OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.H, OAI.ThreeTorus.PhysicalJetData, OAI.ThreeTorus.PhysicalFrame, OAI.ThreeTorus.NeutralStep

  67. abbrev OAI.ThreeTorus.PassagePackets.ModeIndex line 957
  68. def OAI.ThreeTorus.PassagePackets.modeNeg line 959
  69. lemma OAI.ThreeTorus.PassagePackets.modeNeg_involutive line 964
  70. def OAI.ThreeTorus.PassagePackets.modeSum line 969

    Source documentation

    Regroup a literal weighted family by its actual nonzero angular mode. Only algebra is used: no cross-family orthogonality is asserted.

    def modeSum (b : ι → ℂ) : PassagePackets F.ModeIndex :=
…

    Mentions: OAI.ThreeTorus.PassagePackets

  71. lemma OAI.ThreeTorus.PassagePackets.modeSum_good line 974
  72. lemma OAI.ThreeTorus.PassagePackets.modeSum_injective line 977
  73. lemma OAI.ThreeTorus.PassagePackets.modeSum_vector line 979
  74. lemma OAI.ThreeTorus.PassagePackets.modeSum_reflection line 997
  75. def OAI.ThreeTorus.finitePacketSpectralMeasure line 1032

    Source documentation

    The spectral measure is the pushforward of the coefficients' actual energy.

    def finitePacketSpectralMeasure (φ : UnitAddCircle → UnitAddCircle) (m : ι → ℤ)
    (A : ι → UnitAddCircle × UnitAddCircle → ℂ) : Measure UnitAddCircle :=
…
  76. lemma OAI.ThreeTorus.coefficient_memLp_iff line 1037
  77. lemma OAI.ThreeTorus.finitePacketSpectralMeasure_eq_sum line 1046
  78. lemma OAI.ThreeTorus.finitePacket_integral_zero line 1071
  79. lemma OAI.ThreeTorus.finitePacket_twist line 1081
  80. lemma OAI.ThreeTorus.finitePacket_correlation line 1092
  81. lemma OAI.ThreeTorus.coefficient_normsq_eq_physical line 1109
  82. def OAI.ThreeTorus.whitenPackets line 1133
  83. lemma OAI.ThreeTorus.measurable_whitenPackets line 1140
  84. lemma OAI.ThreeTorus.whitenPackets_flat line 1150
  85. lemma OAI.ThreeTorus.memLp_whitenPackets line 1162
  86. lemma OAI.ThreeTorus.whitenPackets_distance line 1175
  87. lemma OAI.ThreeTorus.whitenPackets_reconstruct line 1194
  88. lemma OAI.ThreeTorus.whitenPackets_support line 1208
  89. lemma OAI.ThreeTorus.whitenPackets_reflection line 1224
  90. lemma OAI.ThreeTorus.finitePacketVector_real line 1238