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

Transport of mixed directional quadratic data

This file pulls mixed directional quadratic estimate data across linear isometry equivalences.

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

Pull back mixed-directional quadratic estimate data from an isometric coordinate model.

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

Pull back punctured normalized mixed-directional quadratic estimate data from an isometric coordinate model.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticEstimateAt_comp_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_3} (e : E ≃ₗᵢ[ℝ] F) {D : Finset ι} {v : ι → E} {u : F → ℝ} {x : E} : MixedDirectionalQuadraticEstimateAt D v (u ∘ ⇑e) x ↔ MixedDirectionalQuadraticEstimateAt D (fun (i : ι) => e (v i)) u (e x)

Pointwise transport of mixed-directional quadratic estimate data through a linear isometry equivalence.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticEstimateSet_comp_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_3} (e : E ≃ₗᵢ[ℝ] F) (D : Finset ι) (v : ι → E) (u : F → ℝ) : mixedDirectionalQuadraticEstimateSet D v (u ∘ ⇑e) = ⇑e ⁻¹' mixedDirectionalQuadraticEstimateSet D (fun (i : ι) => e (v i)) u

Set-level transport of mixed-directional quadratic estimate data through a linear isometry equivalence.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticQuotientEstimateAt_comp_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_3} (e : E ≃ₗᵢ[ℝ] F) {D : Finset ι} {v : ι → E} {u : F → ℝ} {x : E} : MixedDirectionalQuadraticQuotientEstimateAt D v (u ∘ ⇑e) x ↔ MixedDirectionalQuadraticQuotientEstimateAt D (fun (i : ι) => e (v i)) u (e x)

Pointwise transport of mixed-directional quotient-estimate data through a linear isometry equivalence.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticQuotientEstimateSet_comp_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_3} (e : E ≃ₗᵢ[ℝ] F) (D : Finset ι) (v : ι → E) (u : F → ℝ) : mixedDirectionalQuadraticQuotientEstimateSet D v (u ∘ ⇑e) = ⇑e ⁻¹' mixedDirectionalQuadraticQuotientEstimateSet D (fun (i : ι) => e (v i)) u

Set-level transport of mixed-directional quotient-estimate data through a linear isometry equivalence.

theorem AleksandrovDifferentiability.PolarizedMixedDirectionalQuadraticEstimateAt.of_image_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_3} [DecidableEq ι] {D : Finset ι} {v : ι → E} {u : E → ℝ} (e : E ≃ₗᵢ[ℝ] F) {x : E} (h : PolarizedMixedDirectionalQuadraticEstimateAt D (fun (i : ι) => e (v i)) (u ∘ ⇑e.symm) (e x)) : PolarizedMixedDirectionalQuadraticEstimateAt D v u x

Pull back polarized mixed-directional quadratic estimate data from an isometric coordinate model.

theorem AleksandrovDifferentiability.PolarizedMixedDirectionalQuadraticQuotientEstimateAt.of_image_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_3} [DecidableEq ι] {D : Finset ι} {v : ι → E} {u : E → ℝ} (e : E ≃ₗᵢ[ℝ] F) {x : E} (h : PolarizedMixedDirectionalQuadraticQuotientEstimateAt D (fun (i : ι) => e (v i)) (u ∘ ⇑e.symm) (e x)) : PolarizedMixedDirectionalQuadraticQuotientEstimateAt D v u x

Pull back punctured normalized polarized mixed-directional quadratic estimate data from an isometric coordinate model.

theorem AleksandrovDifferentiability.polarizedMixedDirectionalQuadraticEstimateAt_comp_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_3} [DecidableEq ι] (e : E ≃ₗᵢ[ℝ] F) {D : Finset ι} {v : ι → E} {u : F → ℝ} {x : E} : PolarizedMixedDirectionalQuadraticEstimateAt D v (u ∘ ⇑e) x ↔ PolarizedMixedDirectionalQuadraticEstimateAt D (fun (i : ι) => e (v i)) u (e x)

Pointwise transport of polarized mixed-directional estimate data through a linear isometry equivalence.

theorem AleksandrovDifferentiability.polarizedMixedDirectionalQuadraticEstimateSet_comp_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_3} [DecidableEq ι] (e : E ≃ₗᵢ[ℝ] F) (D : Finset ι) (v : ι → E) (u : F → ℝ) : polarizedMixedDirectionalQuadraticEstimateSet D v (u ∘ ⇑e) = ⇑e ⁻¹' polarizedMixedDirectionalQuadraticEstimateSet D (fun (i : ι) => e (v i)) u

Set-level transport of polarized mixed-directional estimate data through a linear isometry equivalence.

theorem AleksandrovDifferentiability.polarizedMixedDirectionalQuadraticQuotientEstimateAt_comp_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_3} [DecidableEq ι] (e : E ≃ₗᵢ[ℝ] F) {D : Finset ι} {v : ι → E} {u : F → ℝ} {x : E} : PolarizedMixedDirectionalQuadraticQuotientEstimateAt D v (u ∘ ⇑e) x ↔ PolarizedMixedDirectionalQuadraticQuotientEstimateAt D (fun (i : ι) => e (v i)) u (e x)

Pointwise transport of polarized mixed-directional quotient-estimate data through a linear isometry equivalence.

theorem AleksandrovDifferentiability.polarizedMixedDirectionalQuadraticQuotientEstimateSet_comp_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_3} [DecidableEq ι] (e : E ≃ₗᵢ[ℝ] F) (D : Finset ι) (v : ι → E) (u : F → ℝ) : polarizedMixedDirectionalQuadraticQuotientEstimateSet D v (u ∘ ⇑e) = ⇑e ⁻¹' polarizedMixedDirectionalQuadraticQuotientEstimateSet D (fun (i : ι) => e (v i)) u

Set-level transport of polarized mixed-directional quotient-estimate data through a linear isometry equivalence.