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

Linear-isometry transport for Aleksandrov statement interfaces

theorem AleksandrovDifferentiability.HasSecondOrderExpansionAt.of_image_linearIsometryEquiv {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E ≃ₗᵢ[ℝ] F) {u : E → ℝ} {x : E} {p : F} {B : F →L[ℝ] F} (h : HasSecondOrderExpansionAt (u ∘ ⇑e.symm) (e x) p B) : HasSecondOrderExpansionAt u x (e.symm p) (linearIsometryEquivConjCLM e B)

Pull a concrete second-order expansion back from an isometric coordinate model.

theorem AleksandrovDifferentiability.SecondOrderDifferentiableAt.of_image_linearIsometryEquiv {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E ≃ₗᵢ[ℝ] F) {u : E → ℝ} {x : E} (h : SecondOrderDifferentiableAt (u ∘ ⇑e.symm) (e x)) : SecondOrderDifferentiableAt u x

Pull second-order differentiability back from an isometric coordinate model.

theorem AleksandrovDifferentiability.map_volume_restrict_linearIsometryEquiv_image {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (e : E ≃ₗᵢ[ℝ] F) (Ω : Set E) : MeasureTheory.Measure.map (⇑e) (MeasureTheory.volume.restrict Ω) = MeasureTheory.volume.restrict (⇑e '' Ω)

Restricted volume is preserved by a linear isometry equivalence, with the domain carried to its image.

theorem AleksandrovDifferentiability.ConvexAleksandrovAEStatement.of_image_linearIsometryEquiv {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set E} {u : E → ℝ} (h : ConvexAleksandrovAEStatement F (⇑e '' Ω) (u ∘ ⇑e.symm)) : ConvexAleksandrovAEStatement E Ω u

Pull the final a.e. Aleksandrov statement back from an isometric coordinate model.

theorem AleksandrovDifferentiability.DirectionalLineScalarEstimateSlicewiseStatement.of_image_linearIsometryEquiv {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set E} {u : E → ℝ} (h : DirectionalLineScalarEstimateSlicewiseStatement F (⇑e '' Ω) (u ∘ ⇑e.symm)) : DirectionalLineScalarEstimateSlicewiseStatement E Ω u

Pull a scalar slicewise statement back from an isometric coordinate model.

theorem AleksandrovDifferentiability.DirectionalLineScalarEstimateSlicewiseStatement.image_linearIsometryEquiv {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set E} {u : E → ℝ} (h : DirectionalLineScalarEstimateSlicewiseStatement E Ω u) : DirectionalLineScalarEstimateSlicewiseStatement F (⇑e '' Ω) (u ∘ ⇑e.symm)

Push a scalar slicewise statement forward to an isometric coordinate model.

theorem AleksandrovDifferentiability.DirectionalLineScalarQuotientSlicewiseStatement.of_image_linearIsometryEquiv {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set E} {u : E → ℝ} (h : DirectionalLineScalarQuotientSlicewiseStatement F (⇑e '' Ω) (u ∘ ⇑e.symm)) : DirectionalLineScalarQuotientSlicewiseStatement E Ω u

Pull a scalar quotient slicewise statement back from an isometric coordinate model.

theorem AleksandrovDifferentiability.DirectionalLineScalarQuotientSlicewiseStatement.image_linearIsometryEquiv {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set E} {u : E → ℝ} (h : DirectionalLineScalarQuotientSlicewiseStatement E Ω u) : DirectionalLineScalarQuotientSlicewiseStatement F (⇑e '' Ω) (u ∘ ⇑e.symm)

Push a scalar quotient slicewise statement forward to an isometric coordinate model.

theorem AleksandrovDifferentiability.DirectionalLineScalarEstimateFubiniStatement.of_image_linearIsometryEquiv {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set E} {u : E → ℝ} (h : DirectionalLineScalarEstimateFubiniStatement F (⇑e '' Ω) (u ∘ ⇑e.symm)) : DirectionalLineScalarEstimateFubiniStatement E Ω u

Pull a directional-line scalar Fubini statement back from an isometric coordinate model.

theorem AleksandrovDifferentiability.DirectionalLineScalarQuotientFubiniStatement.of_image_linearIsometryEquiv {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set E} {u : E → ℝ} (h : DirectionalLineScalarQuotientFubiniStatement F (⇑e '' Ω) (u ∘ ⇑e.symm)) : DirectionalLineScalarQuotientFubiniStatement E Ω u

Pull a directional-line scalar quotient Fubini statement back from an isometric coordinate model.

theorem AleksandrovDifferentiability.DirectionalLineScalarUnitFubiniStatement.of_image_linearIsometryEquiv {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set E} {u : E → ℝ} (h : DirectionalLineScalarUnitFubiniStatement F (⇑e '' Ω) (u ∘ ⇑e.symm)) : DirectionalLineScalarUnitFubiniStatement E Ω u

Unit-direction version of DirectionalLineScalarEstimateFubiniStatement.of_image_linearIsometryEquiv.

theorem AleksandrovDifferentiability.DirectionalLineScalarQuotientUnitFubiniStatement.of_image_linearIsometryEquiv {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set E} {u : E → ℝ} (h : DirectionalLineScalarQuotientUnitFubiniStatement F (⇑e '' Ω) (u ∘ ⇑e.symm)) : DirectionalLineScalarQuotientUnitFubiniStatement E Ω u

Unit-direction quotient version of DirectionalLineScalarEstimateFubiniStatement.of_image_linearIsometryEquiv.

theorem AleksandrovDifferentiability.directionalLineScalarSlicewiseTransfer_of_image_linearIsometryEquiv {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set E} {u : E → ℝ} (h : DirectionalLineScalarSlicewiseToFubiniStatement F (⇑e '' Ω) (u ∘ ⇑e.symm)) : DirectionalLineScalarSlicewiseToFubiniStatement E Ω u

Pull a slicewise-to-Fubini transfer theorem back from an isometric coordinate model.

theorem AleksandrovDifferentiability.directionalLineScalarQuotientSlicewiseTransfer_of_image_linearIsometryEquiv {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set E} {u : E → ℝ} (h : DirectionalLineScalarQuotientSlicewiseToFubiniStatement F (⇑e '' Ω) (u ∘ ⇑e.symm)) : DirectionalLineScalarQuotientSlicewiseToFubiniStatement E Ω u

Quotient version of directionalLineScalarSlicewiseTransfer_of_image_linearIsometryEquiv.

theorem AleksandrovDifferentiability.directionalLineScalarUnitSlicewiseTransfer_of_image_linearIsometryEquiv {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set E} {u : E → ℝ} (h : DirectionalLineScalarUnitSlicewiseToFubiniStatement F (⇑e '' Ω) (u ∘ ⇑e.symm)) : DirectionalLineScalarUnitSlicewiseToFubiniStatement E Ω u

Unit-direction version of directionalLineScalarSlicewiseTransfer_of_image_linearIsometryEquiv.

theorem AleksandrovDifferentiability.directionalLineScalarQuotientUnitTransfer_of_image_linearIsometryEquiv {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (e : E ≃ₗᵢ[ℝ] F) {Ω : Set E} {u : E → ℝ} (h : DirectionalLineScalarQuotientUnitSlicewiseToFubiniStatement F (⇑e '' Ω) (u ∘ ⇑e.symm)) : DirectionalLineScalarQuotientUnitSlicewiseToFubiniStatement E Ω u

Unit-direction quotient version of directionalLineScalarSlicewiseTransfer_of_image_linearIsometryEquiv.

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

Pull a finite-family slicewise-to-full-measure transfer theorem back from an isometric coordinate model.

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

Quotient version of finiteDirectionalLineScalarSlicewiseToFullMeasure_of_image_linearIsometryEquiv.

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

Pull a compatible finite-slice full-measure statement back from an isometric coordinate model.

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

Quotient-estimate version of CompatibleDirectionalSliceFullMeasureStatement.of_image_linearIsometryEquiv.

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

Symmetric-compatible version of CompatibleDirectionalSliceFullMeasureStatement.of_image_linearIsometryEquiv.

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

Symmetric-compatible quotient-estimate version of CompatibleDirectionalSliceFullMeasureStatement.of_image_linearIsometryEquiv.