PacketCalculus.lean`

51 declarations, 0 contain sorry, 0 declared as axioms

Trigonometric approximation, spectral calculus, density distances, and reflected clipping.

lemma OAI.ThreeTorus.exists_uniform_laurent line 15

Source documentation

Uniform Laurent approximation of a continuous spectral multiplier.

lemma exists_uniform_laurent {Ψ : UnitAddCircle → ℂ} (hΨ : Continuous Ψ)
    {δ : ℝ} (hd : 0 < δ) :
    ∃ c : ℤ →₀ ℂ, ∀ z, ‖Ψ z-∑ k ∈ c.support, c k*fourier k z‖ < δ := by
…

lemma OAI.ThreeTorus.energy_map_integral_real line 46
lemma OAI.ThreeTorus.finite_energy_measure line 57
lemma OAI.ThreeTorus.packetSpectralMeasure_finite line 64
lemma OAI.ThreeTorus.finitePacket_energy_density line 73
lemma OAI.ThreeTorus.finitePacket_spectral_moment line 84
lemma OAI.ThreeTorus.finitePacket_flat_moment line 98

def OAI.ThreeTorus.multiplyPackets line 108

Source documentation

Actual spectral multiplication of every retained angular coefficient.

def multiplyPackets (φ : UnitAddCircle → UnitAddCircle) (m : ι → ℤ)
    (a : UnitAddCircle → ℂ) (A : ι → UnitAddCircle × UnitAddCircle → ℂ)
    (i : ι) (ua : UnitAddCircle × UnitAddCircle) : ℂ := a (m i • φ ua.1)*A i ua
…

lemma OAI.ThreeTorus.measurable_multiplyPackets line 113
lemma OAI.ThreeTorus.multiplyPackets_spectrum line 119
lemma OAI.ThreeTorus.finitePacketVector_congr_ae line 137
lemma OAI.ThreeTorus.norm_sq_sum_single_live line 157
lemma OAI.ThreeTorus.packetSpectralMeasure_zero line 172
lemma OAI.ThreeTorus.packetSpectralMeasure_sum_disjoint line 176

theorem OAI.ThreeTorus.gather_spectrum line 200

Source documentation

Honest gathering by angular frequency preserves the spectral measure when repeated modes have disjoint physical coefficient supports.

theorem gather_spectrum {ι : Type*} [Fintype ι]
    (m : ι → ℤ) {A : ι → UnitAddCircle × UnitAddCircle → ℂ}
    (hA : ∀ i, Measurable (A i)) (J : Finset ℤ) (hJ : ∀ i, m i ∈ J)
    {φ : UnitAddCircle → UnitAddCircle} (hφ : Measurable φ)
    (hd : ∀ x i j, i ≠ j → m i=m j → A i x=0 ∨ A j x=0) :
    (∑ k : ↥J, packetSpectralMeasure φ k.val
      (fun x => ∑ i, if m i=k.val then A i x else 0)) =
      ∑ i, packetSpectralMeasure φ (m i) (A i) := by
…

Mentions: OAI.ThreeTorus.packetSpectralMeasure

lemma OAI.ThreeTorus.PassagePackets.amplitude_disjoint_of_cylinderCore line 240
lemma OAI.ThreeTorus.l2_integral_norm_sq line 273
lemma OAI.ThreeTorus.integral_norm_product_le line 278
lemma OAI.ThreeTorus.density_norm_bound_l2 line 285
lemma OAI.ThreeTorus.sq_sqrt_sub_sqrt_le_abs line 308
lemma OAI.ThreeTorus.memLp_sqrt_of_integrable line 322
lemma OAI.ThreeTorus.density_hellinger_error line 330
lemma OAI.ThreeTorus.energy_integral_test line 370
lemma OAI.ThreeTorus.integrable_mul_bounded_real line 386

lemma OAI.ThreeTorus.energy_density_difference_le line 397

Source documentation

L¹ contraction for the actual pushed coefficient energies. This proves the paper's density estimate without postulating any abstract spectral map.

lemma energy_density_difference_le {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
    {μ : Measure X} {ν : Measure Y} {ζ : X → Y} {F G : X → ℂ} {p q : Y → ℝ}
    (hζ : Measurable ζ) (hF : Measurable F) (hG : Measurable G)
    (hFl : MemLp F 2 μ) (hGl : MemLp G 2 μ)
    (hp : Measurable p) (hq : Measurable q) (hpi : Integrable p ν) (hqi : Integrable q ν)
    (hpn : ∀ y, 0 ≤ p y) (hqn : ∀ y, 0 ≤ q y)
    (hFp : (μ.withDensity (energyWeight F)).map ζ =
      ν.withDensity (fun y => ENNReal.ofReal (p y)))
    (hGq : (μ.withDensity (energyWeight G)).map ζ =
      ν.withDensity (fun y => ENNReal.ofReal (q y))) :
    (∫ y, |p y-q y| ∂ν) ≤ ∫ x, |‖F x‖^2-‖G x‖^2| ∂μ := by
…

Mentions: OAI.ThreeTorus.μ, OAI.ThreeTorus.energyWeight

lemma OAI.ThreeTorus.density_norm_bound_memLp line 438
lemma OAI.ThreeTorus.coefficient_norm_eq_physical line 463
lemma OAI.ThreeTorus.coefficient_difference_norm line 473

theorem OAI.ThreeTorus.finitePacket_density_distance line 492

Source documentation

The source's constant-one density bound for the literal finite packets, including a nonsmooth old admissible vector.

theorem finitePacket_density_distance {φ : UnitAddCircle → UnitAddCircle}
    (hφ : Measurable φ) {m : ι → ℤ} (hm : Injective m)
    {A B : ι → UnitAddCircle × UnitAddCircle → ℂ}
    (hAm : ∀ i, Measurable (A i)) (hBm : ∀ i, Measurable (B i))
    (hAl : ∀ i, MemLp (A i) 2 slowVolume) (hBl : ∀ i, MemLp (B i) 2 slowVolume)
    {p q : UnitAddCircle → ℝ} (hpm : Measurable p) (hqm : Measurable q)
    (hpi : Integrable p phaseHaar) (hqi : Integrable q phaseHaar)
    (hpn : ∀ z, 0 ≤ p z) (hqn : ∀ z, 0 ≤ q z)
    (hAp : finitePacketSpectralMeasure φ m A = phaseHaar.withDensity (fun z => ENNReal.ofReal (p z)))
    (hBq : finitePacketSpectralMeasure φ m B = phaseHaar.withDensity (fun z => ENNReal.ofReal (q z))) :
    (∫ z, |p z-q z| ∂phaseHaar) ≤
      (‖(memLp_finitePacketVector hAl).toLp (finitePacketVector m A)‖+
…

Mentions: OAI.ThreeTorus.slowVolume, OAI.ThreeTorus.phaseHaar, OAI.ThreeTorus.finitePacketSpectralMeasure, OAI.ThreeTorus.memLp_finitePacketVector, OAI.ThreeTorus.finitePacketVector

lemma OAI.ThreeTorus.gather_vector line 531
lemma OAI.ThreeTorus.PassagePackets.marginalDensity_sum_spectrum line 552

theorem OAI.ThreeTorus.PassagePackets.marginalDensity_distance line 566

Source documentation

L1 spectral density distance for DIFFERENT finite lists. Repeated modes are allowed only with actual disjoint coefficient supports.

theorem marginalDensity_distance (F : PassagePackets ι) (G : PassagePackets κ)
    (hV : G.V=F.V)
    (hF : ∀ x i j, i ≠ j → F.m i=F.m j → F.A i x=0 ∨ F.A j x=0)
    (hG : ∀ x i j, i ≠ j → G.m i=G.m j → G.A i x=0 ∨ G.A j x=0) :
    (∫ z, |(∑ i, F.marginalDensity i z)-(∑ j, G.marginalDensity j z)| ∂phaseHaar) ≤
      (physicalDist (finitePacketVector F.m F.A) 0+physicalDist (finitePacketVector G.m G.A) 0)*
        physicalDist (finitePacketVector F.m F.A) (finitePacketVector G.m G.A) := by
…

Mentions: OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.phaseHaar, OAI.ThreeTorus.physicalDist, OAI.ThreeTorus.finitePacketVector

def OAI.ThreeTorus.reflectedIndexEquiv line 640

Source documentation

Nonzero reflected mode lists are exactly their positive half and its negative copy. This equivalence is used BEFORE the ratio cutoff choices.

def reflectedIndexEquiv {ι : Type*} (m : ι → ℤ) (hm : ∀ i, m i ≠ 0)
    (τ : ι → ι) (hτ : Involutive τ) (hr : ∀ i, m (τ i) = -m i) :
    ({i : ι // 0 < m i} ⊕ {i : ι // 0 < m i}) ≃ ι where
…

lemma OAI.ThreeTorus.sum_reflected_indices line 662
abbrev OAI.ThreeTorus.PositiveIndex line 682
def OAI.ThreeTorus.reflectedVector line 684
lemma OAI.ThreeTorus.reflectedVector_eq line 688
lemma OAI.ThreeTorus.memLp_conj line 701
lemma OAI.ThreeTorus.eLpNorm_conj line 704
lemma OAI.ThreeTorus.reflectedVector_memLp line 708

lemma OAI.ThreeTorus.physicalDist_reflectedVector line 715

Source documentation

A single positive-half coefficient approximation controls the entire real physical vector; the negative half is its exact conjugate copy.

lemma physicalDist_reflectedVector {m : ι → ℤ} (τ : ι → ι)
    {A B : PositiveIndex m → UnitAddCircle × UnitAddCircle → ℂ}
    (hA : ∀ i, MemLp (A i) 2 slowVolume) (hB : ∀ i, MemLp (B i) 2 slowVolume)
    {ε : ℝ} (hε : 0 < ε)
    (he : ∀ i, eLpNorm (fun p => A i p-B i p) 2 slowVolume <
      ENNReal.ofReal ((ε/2)/(Fintype.card (PositiveIndex m)+1))) :
    physicalDist (reflectedVector m τ A) (reflectedVector m τ B) < ε := by
…

Mentions: OAI.ThreeTorus.PositiveIndex, OAI.ThreeTorus.slowVolume, OAI.ThreeTorus.physicalDist, OAI.ThreeTorus.reflectedVector

abbrev OAI.ThreeTorus.RatioPositive line 748
abbrev OAI.ThreeTorus.RatioIndex line 749
def OAI.ThreeTorus.ratioRoot line 751
def OAI.ThreeTorus.ratioCut line 754
def OAI.ThreeTorus.ratioTag line 758
lemma OAI.ThreeTorus.ratioTag_reflect line 761
lemma OAI.ThreeTorus.clipped_reflection line 768
lemma OAI.ThreeTorus.clipped_equal_mode_disjoint line 787
lemma OAI.ThreeTorus.tagged_clipped_vector line 823
lemma OAI.ThreeTorus.untagged_clipped_vector line 839