Averaging an analytic function over a family of contractions

Let f have the power series p on the ball of radius r about c, and let L t, for t ∈ [0, 1], be a continuous family of continuous linear maps of norm at most one. Then the average z ↦ ∫ t in 0..1, f (c + L t (z - c)) has a power series on the same ball, whose n-th coefficient is the average of p n precomposed with L t in every slot (HasFPowerSeriesOnBall.intervalIntegral_comp). In particular the average is analytic at c (AnalyticAt.intervalIntegral_comp).

The typical use is the integral form of Hadamard's lemma: if G (x, y) vanishes on y = y₀, then G (x, y) = (y - y₀) • ∫ t in 0..1, ∂G/∂y (x, y₀ + t (y - y₀)), and this lemma, applied with L t (x, y) = (x, t y), shows that the quotient is again analytic.

theorem HasFPowerSeriesOnBall.intervalIntegral_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F] [CompleteSpace F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {c : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p c r) {L : ℝ → E →L[𝕜] E} (hL : ContinuousOn L (Set.Icc 0 1)) (hL1 : ∀ t ∈ Set.Icc 0 1, ‖L t‖ ≤ 1) : HasFPowerSeriesOnBall (fun (z : E) => ∫ (t : ℝ) in 0..1, f (c + (L t) (z - c))) (fun (n : ℕ) => ∫ (t : ℝ) in 0..1, (p n).compContinuousLinearMap fun (x : Fin n) => L t) c r

If f has the power series p on the ball of radius r about c, and L t is a family of continuous linear maps of norm at most one, continuous in t ∈ [0, 1], then the average z ↦ ∫ t in 0..1, f (c + L t (z - c)) has on the same ball the power series whose n-th coefficient is ∫ t in 0..1, p n ∘ (L t, …, L t).

theorem AnalyticAt.intervalIntegral_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F] [CompleteSpace F] {f : E → F} {c : E} (hf : AnalyticAt 𝕜 f c) {L : ℝ → E →L[𝕜] E} (hL : ContinuousOn L (Set.Icc 0 1)) (hL1 : ∀ t ∈ Set.Icc 0 1, ‖L t‖ ≤ 1) : AnalyticAt 𝕜 (fun (z : E) => ∫ (t : ℝ) in 0..1, f (c + (L t) (z - c))) c

The average z ↦ ∫ t in 0..1, f (c + L t (z - c)) of a function analytic at c, over a family of continuous linear maps of norm at most one, continuous in t ∈ [0, 1], is analytic at c.