Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.
Measure transport for directional estimates #
This file combines isometric measure transport with fixed-direction scalar estimate sets.
theorem
AleksandrovDifferentiability.measure_diff_directionalLineScalarEstimateSet_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 → ℝ}
{v : E}
(hnull : MeasureTheory.volume (Ω \ directionalLineScalarEstimateSet (e v) u) = 0)
:
Pull back full-measure scalar directional-line goodness through a linear isometry equivalence.
This is the measure-theoretic companion to
directionalLineScalarEstimateSet_comp_linearIsometryEquiv.
theorem
AleksandrovDifferentiability.measure_diff_directionalLineScalarQuotientEstimateSet_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 → ℝ}
{v : E}
(hnull : MeasureTheory.volume (Ω \ directionalLineScalarQuotientEstimateSet (e v) u) = 0)
:
Quotient-estimate version of
measure_diff_directionalLineScalarEstimateSet_preimage_linearIsometryEquiv_eq_zero.
theorem
AleksandrovDifferentiability.measure_diff_directionalLineScalarEstimateSet_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 → ℝ}
{v : E}
(hnull : MeasureTheory.volume (⇑e '' Ω \ directionalLineScalarEstimateSet (e v) (u ∘ ⇑e.symm)) = 0)
:
Pull back full-measure scalar directional-line goodness from the image domain of a linear
isometry equivalence. This is the coordinate-change shape used when a problem on Ω is transported
to e '' Ω with function u ∘ e.symm.
theorem
AleksandrovDifferentiability.measure_diff_directionalLineScalarQuotientEstimateSet_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 → ℝ}
{v : E}
(hnull : MeasureTheory.volume (⇑e '' Ω \ directionalLineScalarQuotientEstimateSet (e v) (u ∘ ⇑e.symm)) = 0)
:
Quotient-estimate version of
measure_diff_directionalLineScalarEstimateSet_image_linearIsometryEquiv_eq_zero.
theorem
AleksandrovDifferentiability.measure_diff_directionalSliceEstimateSet_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 (Ω \ directionalSliceEstimateSet D (fun (i : ι) => e (v i)) u) = 0)
:
Pull back full-measure finite directional slice-goodness through a linear isometry equivalence.
theorem
AleksandrovDifferentiability.measure_diff_directionalSliceQuotientEstimateSet_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 (Ω \ directionalSliceQuotientEstimateSet D (fun (i : ι) => e (v i)) u) = 0)
:
Quotient-estimate version of
measure_diff_directionalSliceEstimateSet_preimage_linearIsometryEquiv_eq_zero.
theorem
AleksandrovDifferentiability.measure_diff_directionalSliceEstimateSet_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 '' Ω \ directionalSliceEstimateSet D (fun (i : ι) => e (v i)) (u ∘ ⇑e.symm)) = 0)
:
Pull back full-measure finite directional slice-goodness from the image domain of a linear isometry equivalence.
theorem
AleksandrovDifferentiability.measure_diff_directionalSliceQuotientEstimateSet_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 '' Ω \ directionalSliceQuotientEstimateSet D (fun (i : ι) => e (v i)) (u ∘ ⇑e.symm)) = 0)
:
Quotient-estimate version of
measure_diff_directionalSliceEstimateSet_image_linearIsometryEquiv_eq_zero.
theorem
AleksandrovDifferentiability.measure_diff_compatibleDirectionalSliceEstimateSet_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 (Ω \ compatibleDirectionalSliceEstimateSet D (fun (i : ι) => e (v i)) u) = 0)
:
Pull back full-measure compatible finite directional slice-goodness through a linear isometry equivalence.
theorem
AleksandrovDifferentiability.measure_diff_symmetricCompatibleDirectionalSliceEstimateSet_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 (Ω \ symmetricCompatibleDirectionalSliceEstimateSet D (fun (i : ι) => e (v i)) u) = 0)
:
Symmetric-compatible version of
measure_diff_compatibleDirectionalSliceEstimateSet_preimage_linearIsometryEquiv_eq_zero.
theorem
AleksandrovDifferentiability.measure_diff_compatibleDirectionalSliceQuotientEstimateSet_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 (Ω \ compatibleDirectionalSliceQuotientEstimateSet D (fun (i : ι) => e (v i)) u) = 0)
:
Quotient-estimate version of
measure_diff_compatibleDirectionalSliceEstimateSet_preimage_linearIsometryEquiv_eq_zero.
theorem
AleksandrovDifferentiability.measure_diff_symmetricCompatibleSliceQuotientSet_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 (Ω \ symmetricCompatibleDirectionalSliceQuotientEstimateSet D (fun (i : ι) => e (v i)) u) = 0)
:
MeasureTheory.volume (⇑e ⁻¹' Ω \ symmetricCompatibleDirectionalSliceQuotientEstimateSet D v (u ∘ ⇑e)) = 0
Symmetric-compatible quotient-estimate version of
measure_diff_compatibleDirectionalSliceEstimateSet_preimage_linearIsometryEquiv_eq_zero.
theorem
AleksandrovDifferentiability.measure_diff_compatibleDirectionalSliceEstimateSet_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 '' Ω \ compatibleDirectionalSliceEstimateSet D (fun (i : ι) => e (v i)) (u ∘ ⇑e.symm)) = 0)
:
Pull back full-measure compatible finite directional slice-goodness from the image domain of a linear isometry equivalence.
theorem
AleksandrovDifferentiability.measure_diff_symmetricCompatibleDirectionalSliceEstimateSet_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 '' Ω \ symmetricCompatibleDirectionalSliceEstimateSet D (fun (i : ι) => e (v i)) (u ∘ ⇑e.symm)) = 0)
:
Symmetric-compatible version of
measure_diff_compatibleDirectionalSliceEstimateSet_image_linearIsometryEquiv_eq_zero.
theorem
AleksandrovDifferentiability.measure_diff_compatibleDirectionalSliceQuotientEstimateSet_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 '' Ω \ compatibleDirectionalSliceQuotientEstimateSet D (fun (i : ι) => e (v i)) (u ∘ ⇑e.symm)) = 0)
:
Quotient-estimate version of
measure_diff_compatibleDirectionalSliceEstimateSet_image_linearIsometryEquiv_eq_zero.
theorem
AleksandrovDifferentiability.measure_diff_symmetricCompatibleSliceQuotientSet_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 '' Ω \ symmetricCompatibleDirectionalSliceQuotientEstimateSet D (fun (i : ι) => e (v i)) (u ∘ ⇑e.symm)) = 0)
:
Symmetric-compatible quotient-estimate version of
measure_diff_compatibleDirectionalSliceEstimateSet_image_linearIsometryEquiv_eq_zero.