Exponential decay in s gives L^4 on the cylinder
ProvedFiniteEnergyPlane.memLp_four_of_exp_boundfunctional-analysislp-spacespseudoholomorphic-curves
Let be a normed group, , , and almost everywhere strongly measurable for Lebesgue measure on the strip (cylMeasure). If for all , then .
Role. A convenient membership test for on the cylinder , used for coefficients and weights that decay exponentially at both ends.
Preamble
import Definitions.Def_CauchyRiemannIndex_Setting
Formal statement
namespace FiniteEnergyPlane
open MeasureTheory CauchyRiemannIndex
/-- A strongly measurable `f` on the strip with `‖f (s, t)‖ ≤ C e^{-κ|s|}`, `κ > 0`, lies in
`L⁴(cylMeasure)`. -/
theorem memLp_four_of_exp_bound {E : Type*} [NormedAddCommGroup E] (f : ℝ × ℝ → E)
(hf : AEStronglyMeasurable f cylMeasure) (C κ : ℝ) (hκ : 0 < κ)
(hb : ∀ s t, ‖f (s, t)‖ ≤ C * Real.exp (-(κ * |s|))) : MemLp f 4 cylMeasure := by
sorry
end FiniteEnergyPlane
Source
Setting of C. Wendl, Lectures on Holomorphic Curves in Symplectic and Contact Geometry (arXiv:1011.1690), Ch. 4