Lebesgue integrals over a strip by exhaustion #
The strip ℝ × T is exhausted by the increasing rectangles [-n, n] × T
(TauCeti.iUnion_Icc_neg_prod), so the integrals of a function over these rectangles increase to
its integral over the strip (TauCeti.tendsto_setLIntegral_Icc_neg_prod). If the lower Lebesgue
integral of an ℝ≥0∞-valued function over [-n, n] × T is ENNReal.ofReal (F(n) - F(-n)) for a
real function F with limits A₁ at -∞ and A₂ at ∞, then its integral over the whole strip
is ENNReal.ofReal (A₂ - A₁) (TauCeti.setLIntegral_univ_prod_eq_ofReal_of_tendsto). Since
ENNReal.ofReal truncates at zero, this is A₂ - A₁ when A₁ ≤ A₂ and 0 otherwise.
More generally, a correction term G(n) converging to L may be subtracted on each rectangle,
giving ENNReal.ofReal (A₂ - A₁ - L) (TauCeti.setLIntegral_univ_prod_eq_ofReal_of_tendsto_sub);
the correction term is typically the integral over [-n, n] × T of a function g integrable on
the strip, and then L is the integral of g over the strip
(TauCeti.setLIntegral_univ_prod_eq_ofReal_of_tendsto_sub_integral).
Likewise the half-strip [b, ∞) × T is exhausted by the rectangles [b, b + n] × T: if the
integral over [b, b + n] × T is ENNReal.ofReal (F(b + n) - F(b)) and F tends to L at ∞,
then the integral over the half-strip is ENNReal.ofReal (L - F(b))
(TauCeti.setLIntegral_Ici_prod_eq_ofReal_of_tendsto).
This is the passage from the energy identity on finite rectangles to the energy of a holomorphic strip or a Floer cylinder, whose energy is the difference of the limiting actions at its two ends, and of a Floer half-cylinder.
The strip is also the union of the disjoint translates of a period rectangle
(a, a + c] × T. A function on the strip that is periodic in the first variable has the same
integral over each translate, so if its integral over the strip is finite, then its integral over
each period rectangle vanishes, and hence so does its integral over the whole strip
(TauCeti.setLIntegral_univ_prod_eq_zero_of_periodic). For the energy density of a Floer cylinder
this says that a finite-energy cylinder invariant under a nontrivial translation has zero
energy.
Finally, a function with finite integral over a set E has small integral over the parts of E
far out along the strip: its integrals over sets that eventually lie in E and outside every band
|z.1| < R tend to zero (TauCeti.tendsto_setLIntegral_of_eventually_subset). Applied to
windows [a + s_k, b + s_k] × T with |s_k| → ∞, this says that a half-cylinder of finite energy
carries less and less energy over its translated windows, since such windows eventually lie
outside every band (TauCeti.eventually_Icc_add_prod_subset_inter).
The integrals of f over the rectangles [-n, n] × T increase to its integral over the
strip ℝ × T.
Integrals over a strip by exhaustion, with a correction term. If the integral of f over
each rectangle [-n, n] × T is ENNReal.ofReal (F(n) - F(-n) - G(n)), where F tends to A₁ at
-∞ and to A₂ at ∞ and G(n) tends to L, then the integral of f over the strip ℝ × T is
ENNReal.ofReal (A₂ - A₁ - L).
Integrals over a strip by exhaustion. If the integral of f over each rectangle
[-n, n] × T is ENNReal.ofReal (F(n) - F(-n)), where F tends to A₁ at -∞ and to A₂ at
∞, then the integral of f over the strip ℝ × T is ENNReal.ofReal (A₂ - A₁), that is
A₂ - A₁ truncated at zero.
Integrals over a strip by exhaustion, with an integral correction term. Let g be
integrable on the strip ℝ × T, for measurable T. If the integral of f over each rectangle
[-n, n] × T is ENNReal.ofReal (F(n) - F(-n) - ∫_{[-n, n] × T} g), where F tends to A₁ at
-∞ and to A₂ at ∞, then the integral of f over the strip is
ENNReal.ofReal (A₂ - A₁ - ∫_{ℝ × T} g).
Integrals over a half-strip by exhaustion. If the integral of f over each rectangle
[b, b + n] × T is ENNReal.ofReal (F(b + n) - F(b)), where F tends to L at ∞, then the
integral of f over the half-strip [b, ∞) × T is ENNReal.ofReal (L - F(b)), that is
L - F(b) truncated at zero.
Periodic functions on a strip. Let μ be a measure on ℝ × β invariant under the
translation (s, t) ↦ (s + c, t) for some c > 0, and let f be periodic in s with period c
on the strip ℝ × T. If the integral of f over the strip is finite, then it is zero. No
measurability of f is assumed.
If |s_i| → ∞ and the translated window [a + s_i, b + s_i] × T eventually lies in E, then
it eventually lies in E and outside the band |z.1| < R, for every R. These windows are thus
sets to which TauCeti.tendsto_setLIntegral_of_eventually_subset applies.
Integrals over sets escaping along the strip. If f has finite integral over E, then its
integrals over sets A i that eventually lie in E and outside every band |z.1| < R tend to
zero. For the energy density of a half-cylinder of finite energy, this says that the energy over
a window translated towards the end tends to zero. No measurability of f, E or A i is
assumed.