English
Under similar hypotheses as above, the same identity for regionBetween holds, equating a product-ruled volume with the integral of g − f over s.
Русский
При аналогичных предположениях сохраняется та же формула: объем области между f и g равен интегралу от (g − f) на s.
LaTeX
$$$\mu \times\mathrm{volume}(\mathrm{regionBetween}(f,g,s)) = \mathrm{ENNReal.ofReal}\left( \int_s (g - f) \, d\mu \right)$$$
Lean4
theorem volume_sum_rpow_le [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₁ : 0 < p := by
linarith
-- We collect facts about `Lp` norms that will be used in `measure_le_one_eq_lt_one`
have eq_norm := fun x : ι → ℝ =>
(PiLp.norm_eq_sum (p := .ofReal p) (f := x) ((toReal_ofReal (le_of_lt h₁)).symm ▸ h₁))
simp_rw [toReal_ofReal (le_of_lt h₁), Real.norm_eq_abs] at eq_norm
have : Fact (1 ≤ ENNReal.ofReal p) := fact_iff.mpr (ofReal_one ▸ (ofReal_le_ofReal hp))
have nm_zero := norm_zero (E := PiLp (.ofReal p) (fun _ : ι => ℝ))
have eq_zero := fun x : ι → ℝ => norm_eq_zero (E := PiLp (.ofReal p) (fun _ : ι => ℝ)) (a := x)
have nm_neg := fun x : ι → ℝ => norm_neg (E := PiLp (.ofReal p) (fun _ : ι => ℝ)) x
have nm_add := fun x y : ι → ℝ => norm_add_le (E := PiLp (.ofReal p) (fun _ : ι => ℝ)) x y
simp_rw [eq_norm] at eq_zero nm_zero nm_neg nm_add
have nm_smul := fun (r : ℝ) (x : ι → ℝ) => norm_smul_le (β := PiLp (.ofReal p) (fun _ : ι => ℝ)) r x
simp_rw [eq_norm, norm_eq_abs] at nm_smul
rw [measure_le_eq_lt _ nm_zero (fun x ↦ nm_neg x) (fun x y ↦ nm_add x y) (eq_zero _).mp (fun r x => nm_smul r x),
volume_sum_rpow_lt _ hp]
