Backward transport on positive windows. No continuity at zero is needed when the source integral is uniformly bounded on every such window.
theorem
AVenhance.Infra.Section5.RelativeError.relative_initial_backward_transport_integrated_pos
{F source : ℝ → Homogenization.Vec 2 → ℝ}
(X : ℝ → Ergodic.PeriodicVolumePreservingDiffeomorphism 2)
(hFper : ∀ (t : ℝ), IsZ2Periodic (F t))
(hSourcePer : ∀ (t : ℝ), IsZ2Periodic (source t))
(hComp : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => F p.1 ((X p.1).toFun p.2)) (Set.Ioi 0 ×ˢ Set.univ))
(hSourceComp :
ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => source p.1 ((X p.1).toFun p.2)) (Set.Ioi 0 ×ˢ Set.univ))
(hMaterial :
∀ (t : ℝ),
0 < t → ∀ (x : Homogenization.Vec 2), HasDerivAt (fun (s : ℝ) => F s ((X s).toFun x)) (source t ((X t).toFun x)) t)
{b D : ℝ}
(hb : 0 < b)
(hD : 0 ≤ D)
(hzero : F b = 0)
(hSourceIntegral : ∀ t ∈ Set.Ioc 0 b, ∫ (s : ℝ) in t..b, √(l2NormSq (source s)) ≤ D)
(t : ℝ)
:
Backward FTC and compact maximum absorption control every positive slice.
The source primitive is bounded on [t,b], so the argument never uses time zero.
theorem
AVenhance.Infra.Section5.RelativeError.relative_initial_source_L1_of_positive_L2
{t b D : ℝ}
(ht : 0 < t)
(htb : t ≤ b)
(hD : 0 ≤ D)
{g : ℝ → ℝ}
(hg : ContinuousOn g (Set.Icc t b))
(hquad : ∫ (s : ℝ) in t..b, g s ^ 2 ≤ D ^ 2)
:
Time Cauchy--Schwarz on a positive subwindow, with an abstract source amplitude. No source trace at zero is assumed.