Monotonicity of the composed-analyticity hypothesis of l.flow.averages: a larger amplitude
and a smaller radius weaken it.
theorem
AVenhance.Infra.Section5.AnalyticBridge.hasCoordinateAnalyticL1Bounds_mono
{d : ℕ}
{f : Homogenization.Vec d → ℂ}
{Cf r Cf' r' : ℝ}
(h : Ergodic.HasCoordinateAnalyticL1Bounds f Cf r)
(hC : Cf ≤ Cf')
(hC' : 0 ≤ Cf')
(hr' : 0 < r')
(hr : r' ≤ r)
: