Torus and volume mean values on polydiscs

The fixed-radius torus average of a holomorphic function equals its value at the center, for every valid radius. This is the plain Bochner-integral average, with no residual Jacobian factor: the complex contour normalization in torusIntegral cancels exactly at the center. Averaging common complex rotations and applying Fubini also gives the volume mean-value formula on equal-radius polydiscs. This formula supports the local Lp estimate on holomorphic function spaces. Arbitrary finite coordinate types, including the empty type, are allowed in the volume formula.

Main results

• torusAverage_eq_center: At the center of a polydisc, the fixed-radius torus average is a plain Bochner-integral average of the function over the angle cube, with no Jacobian residue.
• integral_closedBall_zero_eq_volume_smul: Averaging a holomorphic function over an equal-radius polydisc centered at zero returns its center value times the volume.
• integral_closedBall_eq_volume_smul: The volume mean-value formula on an equal-radius polydisc with arbitrary center.

theorem SeveralComplexVariables.torusAverage_eq_center {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {d : ℕ} {f : (Fin d → ℂ) → E} {c : Fin d → ℂ} {R : Fin d → ℝ} (hR : ∀ (i : Fin d), 0 < R i) (hfc : ContinuousOn f (closedPolydisc c R)) (hfa : ∀ z ∈ closedPolydisc c R, ∀ (i : Fin d), AnalyticAt ℂ (fun (x : ℂ) => f (Function.update z i x)) (z i)) : ∫ (θ : Fin d → ℝ) in Set.Icc 0 fun (x : Fin d) => 2 * Real.pi, f (torusMap c R θ) = (2 * ↑Real.pi) ^ d • f c

At the center of a polydisc, the fixed-radius torus average is a plain Bochner-integral average of the function over the angle cube, with no Jacobian residue.

theorem SeveralComplexVariables.integral_closedBall_zero_eq_volume_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {ι : Type u_2} [Fintype ι] {f : (ι → ℂ) → E} {r : ℝ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 r)) : ∫ (z : ι → ℂ) in Metric.closedBall 0 r, f z = MeasureTheory.volume.real (Metric.closedBall 0 r) • f 0

Averaging a holomorphic function over an equal-radius polydisc centered at zero returns its center value times the volume. The proof averages common complex rotations and uses Fubini; it also applies when the coordinate type is empty.

theorem SeveralComplexVariables.integral_closedBall_eq_volume_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {ι : Type u_2} [Fintype ι] {f : (ι → ℂ) → E} {c : ι → ℂ} {r : ℝ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall c r)) : ∫ (z : ι → ℂ) in Metric.closedBall c r, f z = MeasureTheory.volume.real (Metric.closedBall c r) • f c

The volume mean-value formula on an equal-radius polydisc with arbitrary center. The norm on the finite coordinate space is the supremum norm.