Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.

Measure transport under linear isometries

This file records null-set transport lemmas for Lebesgue volume under linear isometry equivalences.

theorem AleksandrovDifferentiability.measure_preimage_linearIsometryEquiv_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] (e : E ≃ₗᵢ[ℝ] F) {s : Set F} (hs : MeasureTheory.volume s = 0) : MeasureTheory.volume (⇑e ⁻¹' s) = 0

A linear isometry equivalence preserves null preimages for Lebesgue volume.

theorem AleksandrovDifferentiability.measure_diff_quadraticEstimateSet_preimage_linearIsometryEquiv_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set F} {u : F → ℝ} (hnull : MeasureTheory.volume (Ω \ quadraticEstimateSet u) = 0) : MeasureTheory.volume (⇑e ⁻¹' Ω \ quadraticEstimateSet (u ∘ ⇑e)) = 0

Pull back full-measure ambient quadratic estimate goodness through a linear isometry equivalence.

theorem AleksandrovDifferentiability.measure_diff_quadraticQuotientEstimateSet_preimage_linearIsometryEquiv_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set F} {u : F → ℝ} (hnull : MeasureTheory.volume (Ω \ quadraticQuotientEstimateSet u) = 0) : MeasureTheory.volume (⇑e ⁻¹' Ω \ quadraticQuotientEstimateSet (u ∘ ⇑e)) = 0

Quotient-estimate version of measure_diff_quadraticEstimateSet_preimage_linearIsometryEquiv_eq_zero.

theorem AleksandrovDifferentiability.measure_diff_quadraticEstimateSet_image_linearIsometryEquiv_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set E} {u : E → ℝ} (hnull : MeasureTheory.volume (⇑e '' Ω \ quadraticEstimateSet (u ∘ ⇑e.symm)) = 0) : MeasureTheory.volume (Ω \ quadraticEstimateSet u) = 0

Pull back full-measure ambient quadratic estimate goodness from the image domain of a linear isometry equivalence.

theorem AleksandrovDifferentiability.measure_diff_quadraticQuotientEstimateSet_image_linearIsometryEquiv_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set E} {u : E → ℝ} (hnull : MeasureTheory.volume (⇑e '' Ω \ quadraticQuotientEstimateSet (u ∘ ⇑e.symm)) = 0) : MeasureTheory.volume (Ω \ quadraticQuotientEstimateSet u) = 0

Quotient-estimate version of measure_diff_quadraticEstimateSet_image_linearIsometryEquiv_eq_zero.

theorem AleksandrovDifferentiability.measure_diff_mixedDirectionalQuadraticEstimateSet_preimage_linearIsometryEquiv_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_3} [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set F} {D : Finset ι} {v : ι → E} {u : F → ℝ} (hnull : MeasureTheory.volume (Ω \ mixedDirectionalQuadraticEstimateSet D (fun (i : ι) => e (v i)) u) = 0) : MeasureTheory.volume (⇑e ⁻¹' Ω \ mixedDirectionalQuadraticEstimateSet D v (u ∘ ⇑e)) = 0

Pull back full-measure mixed-directional estimate goodness through a linear isometry equivalence.

theorem AleksandrovDifferentiability.measure_diff_mixedDirectionalQuadraticQuotientSet_preimage_linearIsometryEquiv_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_3} [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set F} {D : Finset ι} {v : ι → E} {u : F → ℝ} (hnull : MeasureTheory.volume (Ω \ mixedDirectionalQuadraticQuotientEstimateSet D (fun (i : ι) => e (v i)) u) = 0) : MeasureTheory.volume (⇑e ⁻¹' Ω \ mixedDirectionalQuadraticQuotientEstimateSet D v (u ∘ ⇑e)) = 0

Quotient-estimate version of measure_diff_mixedDirectionalQuadraticEstimateSet_preimage_linearIsometryEquiv_eq_zero.

theorem AleksandrovDifferentiability.measure_diff_polarizedMixedDirectionalQuadraticSet_preimage_linearIsometryEquiv_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_3} [DecidableEq ι] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set F} {D : Finset ι} {v : ι → E} {u : F → ℝ} (hnull : MeasureTheory.volume (Ω \ polarizedMixedDirectionalQuadraticEstimateSet D (fun (i : ι) => e (v i)) u) = 0) : MeasureTheory.volume (⇑e ⁻¹' Ω \ polarizedMixedDirectionalQuadraticEstimateSet D v (u ∘ ⇑e)) = 0

Pull back full-measure polarized mixed-directional estimate goodness through a linear isometry equivalence.

theorem AleksandrovDifferentiability.measure_diff_polarizedMixedDirectionalQuotientSet_preimage_linearIsometryEquiv_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_3} [DecidableEq ι] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set F} {D : Finset ι} {v : ι → E} {u : F → ℝ} (hnull : MeasureTheory.volume (Ω \ polarizedMixedDirectionalQuadraticQuotientEstimateSet D (fun (i : ι) => e (v i)) u) = 0) : MeasureTheory.volume (⇑e ⁻¹' Ω \ polarizedMixedDirectionalQuadraticQuotientEstimateSet D v (u ∘ ⇑e)) = 0

Quotient-estimate version of measure_diff_polarizedMixedDirectionalQuadraticSet_preimage_linearIsometryEquiv_eq_zero.

theorem AleksandrovDifferentiability.measure_diff_mixedDirectionalQuadraticEstimateSet_image_linearIsometryEquiv_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_3} [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set E} {D : Finset ι} {v : ι → E} {u : E → ℝ} (hnull : MeasureTheory.volume (⇑e '' Ω \ mixedDirectionalQuadraticEstimateSet D (fun (i : ι) => e (v i)) (u ∘ ⇑e.symm)) = 0) : MeasureTheory.volume (Ω \ mixedDirectionalQuadraticEstimateSet D v u) = 0

Pull back full-measure mixed-directional estimate goodness from the image domain of a linear isometry equivalence.

theorem AleksandrovDifferentiability.measure_diff_mixedDirectionalQuadraticQuotientSet_image_linearIsometryEquiv_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_3} [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set E} {D : Finset ι} {v : ι → E} {u : E → ℝ} (hnull : MeasureTheory.volume (⇑e '' Ω \ mixedDirectionalQuadraticQuotientEstimateSet D (fun (i : ι) => e (v i)) (u ∘ ⇑e.symm)) = 0) : MeasureTheory.volume (Ω \ mixedDirectionalQuadraticQuotientEstimateSet D v u) = 0

Quotient-estimate version of measure_diff_mixedDirectionalQuadraticEstimateSet_image_linearIsometryEquiv_eq_zero.

theorem AleksandrovDifferentiability.measure_diff_polarizedMixedDirectionalQuadraticSet_image_linearIsometryEquiv_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_3} [DecidableEq ι] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set E} {D : Finset ι} {v : ι → E} {u : E → ℝ} (hnull : MeasureTheory.volume (⇑e '' Ω \ polarizedMixedDirectionalQuadraticEstimateSet D (fun (i : ι) => e (v i)) (u ∘ ⇑e.symm)) = 0) : MeasureTheory.volume (Ω \ polarizedMixedDirectionalQuadraticEstimateSet D v u) = 0

Pull back full-measure polarized mixed-directional estimate goodness from the image domain of a linear isometry equivalence.

theorem AleksandrovDifferentiability.measure_diff_polarizedMixedDirectionalQuotientSet_image_linearIsometryEquiv_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_3} [DecidableEq ι] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set E} {D : Finset ι} {v : ι → E} {u : E → ℝ} (hnull : MeasureTheory.volume (⇑e '' Ω \ polarizedMixedDirectionalQuadraticQuotientEstimateSet D (fun (i : ι) => e (v i)) (u ∘ ⇑e.symm)) = 0) : MeasureTheory.volume (Ω \ polarizedMixedDirectionalQuadraticQuotientEstimateSet D v u) = 0

Quotient-estimate version of measure_diff_polarizedMixedDirectionalQuadraticSet_image_linearIsometryEquiv_eq_zero.