English
The regionBetween(f,g,s) consists of all (x,t) with x ∈ s and t ∈ Ioo(f x)(g x); i.e., points whose second coordinate lies strictly between f(x) and g(x).
Русский
regionBetween(f,g,s) состоит из всех пар (x,t), где x ∈ s и t лежит строго между f(x) и g(x).
LaTeX
$$$$ \\operatorname{regionBetween}(f,g,s) = \\{ (x,t) : x \\in s \\text{ and } t \\in Ioo(f(x),g(x)) \\}. $$$$
Lean4
/-- Any invertible matrix rescales Lebesgue measure through the absolute value of its
determinant. -/
theorem map_matrix_volume_pi_eq_smul_volume_pi [DecidableEq ι] {M : Matrix ι ι ℝ} (hM : det M ≠ 0) :
Measure.map (toLin' M) volume = ENNReal.ofReal (abs (det M)⁻¹) • volume := by
-- This follows from the cases we have already proved, of diagonal matrices and transvections,
-- as these matrices generate all invertible matrices.
apply diagonal_transvection_induction_of_det_ne_zero _ M hM
· intro D hD
conv_rhs => rw [← smul_map_diagonal_volume_pi hD]
rw [smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, inv_mul_cancel₀ hD, abs_one, ENNReal.ofReal_one,
one_smul]
· intro t
simp_rw [Matrix.TransvectionStruct.det, _root_.inv_one, abs_one, ENNReal.ofReal_one, one_smul,
(volume_preserving_transvectionStruct _).map_eq]
· intro A B _ _ IHA IHB
rw [toLin'_mul, det_mul, LinearMap.coe_comp, ← Measure.map_map, IHB, Measure.map_smul, IHA, smul_smul, ←
ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, mul_comm, mul_inv]
· apply Continuous.measurable
apply LinearMap.continuous_on_pi
· apply Continuous.measurable
apply LinearMap.continuous_on_pi
