Abstract integration by parts in time (s.indy#Q-primitive, s.indy#ibp-in-time) #
Source: enhance.tex 8700–8830. A mean-zero P-periodic continuous function G with
N P = 1 has the primitive Q(t) = ∫_0^t G, which is bounded by P ‖G‖_∞ and vanishes at
t = 0 and t = 1; integrating by parts against an absolutely-differentiable A gives
|∫_0^1 G A| ≤ P ‖G‖_∞ ∫_0^1 |A'|.
theorem
AVenhance.Infra.Section5.LeftToShow.integral_period_eq_zero_of_unit
{G : ℝ → ℝ}
{P : ℝ}
{N : ℕ}
(hNP : ↑N * P = 1)
(hG : Continuous G)
(hGper : Function.Periodic G P)
(hGmean : ∫ (t : ℝ) in 0..1, G t = 0)
:
A P-periodic function with N P = 1 that has mean zero on [0,1] has mean zero on a
single period.
theorem
AVenhance.Infra.Section5.LeftToShow.abs_intervalIntegral_mul_le_of_periodic_mean_zero
{G A A' : ℝ → ℝ}
{P B : ℝ}
{N : ℕ}
(hP : 0 < P)
(hNP : ↑N * P = 1)
(hG : Continuous G)
(hGper : Function.Periodic G P)
(hGmean : ∫ (t : ℝ) in 0..1, G t = 0)
(hB : ∀ (t : ℝ), |G t| ≤ B)
(hA : ContinuousOn A (Set.Icc 0 1))
(hA' : ∀ t ∈ Set.Ioo 0 1, HasDerivAt A (A' t) t)
(hA'int : IntervalIntegrable A' MeasureTheory.volume 0 1)
:
Abstract s.indy#Q-primitive + s.indy#ibp-in-time.