English
If f and g are integrable on s and s is measurable, then the regionBetween integral identity holds: the volume equals the integral of g − f over s.
Русский
Если f и g интегрируемы на s и s измеримо, то выполняется равенство объема области между f и g и интеграла от (g − f) по s.
LaTeX
$$$\mu \cdot \mathrm{volume}(\mathrm{regionBetween}(f,g,s)) = \mathrm{ENNReal.ofReal}\left( \int_s (g - f) \, d\mu \right)$$$
Lean4
theorem volume_sum_rpow_lt [Nonempty ι] {p : ℝ} (hp : 1 ≤ p) (r : ℝ) :
volume {x : ι → ℝ | (∑ i, |x i| ^ p) ^ (1 / p) < r} =
(.ofReal r) ^ card ι * .ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (card ι / p + 1)) :=
by
have h₁ (x : ι → ℝ) : 0 ≤ ∑ i, |x i| ^ p := by positivity
have h₂ : ∀ x : ι → ℝ, 0 ≤ (∑ i, |x i| ^ p) ^ (1 / p) := fun x => rpow_nonneg (h₁ x) _
obtain hr | hr := le_or_gt r 0
· have : {x : ι → ℝ | (∑ i, |x i| ^ p) ^ (1 / p) < r} = ∅ :=
by
ext x
refine ⟨fun hx => ?_, fun hx => hx.elim⟩
exact not_le.mpr (lt_of_lt_of_le (Set.mem_setOf.mp hx) hr) (h₂ x)
rw [this, measure_empty, ← zero_eq_ofReal.mpr hr, zero_pow Fin.pos'.ne', zero_mul]
· rw [← volume_sum_rpow_lt_one _ hp, ← ofReal_pow (le_of_lt hr), ← finrank_pi ℝ]
convert addHaar_smul_of_nonneg volume (le_of_lt hr) {x : ι → ℝ | ∑ i, |x i| ^ p < 1} using 2
simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hr), Set.preimage_setOf_eq, Pi.smul_apply, smul_eq_mul, abs_mul,
mul_rpow (abs_nonneg _) (abs_nonneg _), abs_inv, inv_rpow (abs_nonneg _), ← Finset.mul_sum,
abs_eq_self.mpr (le_of_lt hr), inv_mul_lt_iff₀ (rpow_pos_of_pos hr _), mul_one, ←
rpow_lt_rpow_iff (rpow_nonneg (h₁ _) _) (le_of_lt hr) (by linarith : 0 < p), ← rpow_mul (h₁ _),
div_mul_cancel₀ _ (ne_of_gt (by linarith) : p ≠ 0), Real.rpow_one]
