Theorems · Theorem · several complex variables

norm_torusIntegral_le_of_norm_le_const

∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : (Fin n → ℂ) → E} {c : Fin n → ℂ}
  {R : Fin n → ℝ} {C : ℝ},
  (∀ (θ : Fin n → ℝ), ‖f (torusMap c R θ)‖ ≤ C) →
    ‖∯ (x : Fin n → ℂ) in T(c, R), f x‖ ≤ ((2 * Real.pi) ^ n * ∏ i, |R i|) * C

If for all θ : ℝⁿ, ‖f (torusMap c R θ)‖ is less than or equal to a constant C : ℝ, then ‖∯ x in T(c, R), f x‖ is less than or equal to (2 * π)^n * (∏ i, |R i|) * C

Defined in

Mathlib.MeasureTheory.Integral.TorusIntegral

Cited by

0 results in Mathlib

Foundations

Depth 260 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace