PacketLatticeAverage.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Averaging actual packet sums over one sheared lattice cell. The probability normalization leaves precisely one inverse area per packet.

theorem OAI.LipschitzHilbert.PacketRepresentation.averaged_packet_identity line 12

theorem OAI.LipschitzHilbert.PacketRepresentation.averaged_packet_bound line 40

Source documentation

Uniform bounds for the finite packet forms pass to the actual averaged convolution form. Absolute convergence, rather than a cardinality bound, justifies the passage through the infinite spatial lattice.

theorem averaged_packet_bound (KA KB f b g : ℝ × ℝ → ℂ)
    (hA : Integrable KA planeMeasure) (hB : Integrable KB planeMeasure)
    (hf : Integrable f planeMeasure) (hb : Measurable b) (hg : Measurable g)
    (Mb Mg : ℝ) (hbb : ∀ x, ‖b x‖≤Mb) (hgb : ∀ x, ‖g x‖≤Mg)
    (l W theta C : ℝ) (hl : 0<l) (hW : 0<W)
    (hfinite : ∀ z (I : Finset (ℤ×ℤ)),
      ‖∑ n∈I, ((l*W:ℝ):ℂ)⁻¹ *
        packetProduct KA KB f b g (l*W) (latticeHom l W theta n+z)‖≤C) :
    ‖∫ x, b x*kernelConvolution KA (kernelConvolution KB f) x*conj (g x) ∂planeMeasure‖≤C := by
…

Mentions: OAI.LipschitzHilbert.PacketRepresentation.planeMeasure, OAI.LipschitzHilbert.PacketRepresentation.packetProduct, OAI.LipschitzHilbert.PacketRepresentation.latticeHom, OAI.LipschitzHilbert.PacketRepresentation.kernelConvolution