From 4b884eff88bf72d32496b0bc7cc0bfccce77f2fa Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 15 May 2023 07:08:24 +0000 Subject: [PATCH] chore(measure_theory/measure/haar_of_basis): lemmas about `basis.parallelepiped` (#18873) These are bundled versions of the lemmas about `parallelepiped`. This is working towards the result that the measure on `euclidean_space` and the corresponding pi type agree. --- src/measure_theory/measure/haar_of_basis.lean | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/src/measure_theory/measure/haar_of_basis.lean b/src/measure_theory/measure/haar_of_basis.lean index dfbf34e1b7ff7..3da1e80196ca2 100644 --- a/src/measure_theory/measure/haar_of_basis.lean +++ b/src/measure_theory/measure/haar_of_basis.lean @@ -179,7 +179,7 @@ end add_comm_group section normed_space -variables [normed_add_comm_group E] [normed_space ℝ E] +variables [normed_add_comm_group E] [normed_add_comm_group F] [normed_space ℝ E] [normed_space ℝ F] /-- The parallelepiped spanned by a basis, as a compact set with nonempty interior. -/ def basis.parallelepiped (b : basis ι ℝ E) : positive_compacts E := @@ -200,6 +200,23 @@ def basis.parallelepiped (b : basis ι ℝ E) : positive_compacts E := rwa [← homeomorph.image_interior, nonempty_image_iff], end } +@[simp] lemma basis.coe_parallelepiped (b : basis ι ℝ E) : + (b.parallelepiped : set E) = parallelepiped b := +rfl + +@[simp] lemma basis.parallelepiped_reindex (b : basis ι ℝ E) (e : ι ≃ ι') : + (b.reindex e).parallelepiped = b.parallelepiped := +positive_compacts.ext $ + (congr_arg parallelepiped (b.coe_reindex _)).trans (parallelepiped_comp_equiv b e.symm) + +lemma basis.parallelepiped_map (b : basis ι ℝ E) (e : E ≃ₗ[ℝ] F) : + (b.map e).parallelepiped = b.parallelepiped.map e + (by haveI := finite_dimensional.of_fintype_basis b; exact + e.to_linear_map.continuous_of_finite_dimensional) + (by haveI := finite_dimensional.of_fintype_basis (b.map e); exact + e.to_linear_map.is_open_map_of_finite_dimensional e.surjective) := +positive_compacts.ext (image_parallelepiped e.to_linear_map _).symm + variables [measurable_space E] [borel_space E] /-- The Lebesgue measure associated to a basis, giving measure `1` to the parallelepiped spanned