Ehrhart volume inequality: FourierAnalysis

Fourier, Dolbeault, and weighted Bochner estimates.

theorem Ehrhart.MatrixTorusBochnerCoreConvergence.complexLp_norm_le_of_ae_norm_le {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : X → E} {g : X → F} (hf : MeasureTheory.MemLp f 2 μ) (hg : MeasureTheory.MemLp g 2 μ) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C * ‖g x‖) : ‖MeasureTheory.MemLp.toLp f hf‖ ≤ C * ‖MeasureTheory.MemLp.toLp g hg‖

Almost-everywhere norm domination gives the corresponding L² norm bound.