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

Directional estimate transport

This file proves pointwise and set-level transport lemmas for fixed-direction scalar estimate sets under linear isometry equivalences.

theorem AleksandrovDifferentiability.mem_directionalLineScalarEstimateSet_comp_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) {u : F → ℝ} {x v : E} : x ∈ directionalLineScalarEstimateSet v (u ∘ ⇑e) ↔ e x ∈ directionalLineScalarEstimateSet (e v) u

Pointwise transport of the fixed-direction scalar line-good predicate through a linear isometry equivalence.

theorem AleksandrovDifferentiability.directionalLineScalarEstimateSet_comp_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) (u : F → ℝ) (v : E) : directionalLineScalarEstimateSet v (u ∘ ⇑e) = ⇑e ⁻¹' directionalLineScalarEstimateSet (e v) u

Set-level transport of the fixed-direction scalar line-good predicate through a linear isometry equivalence.

theorem AleksandrovDifferentiability.mem_directionalLineScalarQuotientEstimateSet_comp_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) {u : F → ℝ} {x v : E} : x ∈ directionalLineScalarQuotientEstimateSet v (u ∘ ⇑e) ↔ e x ∈ directionalLineScalarQuotientEstimateSet (e v) u

Pointwise transport of the fixed-direction scalar quotient line-good predicate through a linear isometry equivalence.

theorem AleksandrovDifferentiability.directionalLineScalarQuotientEstimateSet_comp_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) (u : F → ℝ) (v : E) : directionalLineScalarQuotientEstimateSet v (u ∘ ⇑e) = ⇑e ⁻¹' directionalLineScalarQuotientEstimateSet (e v) u

Set-level transport of the fixed-direction scalar quotient line-good predicate through a linear isometry equivalence.

theorem AleksandrovDifferentiability.mem_directionalSliceEstimateSet_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} : x ∈ directionalSliceEstimateSet D v (u ∘ ⇑e) ↔ e x ∈ directionalSliceEstimateSet D (fun (i : ι) => e (v i)) u

Pointwise transport of finite directional slice-good data through a linear isometry equivalence.

theorem AleksandrovDifferentiability.directionalSliceEstimateAt_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} : DirectionalSliceEstimateAt D v (u ∘ ⇑e) x ↔ DirectionalSliceEstimateAt D (fun (i : ι) => e (v i)) u (e x)

Pointwise transport of finite directional slice data through a linear isometry equivalence.

theorem AleksandrovDifferentiability.directionalSliceEstimateSet_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 → ℝ) : directionalSliceEstimateSet D v (u ∘ ⇑e) = ⇑e ⁻¹' directionalSliceEstimateSet D (fun (i : ι) => e (v i)) u

Set-level transport of finite directional slice-good data through a linear isometry equivalence.

theorem AleksandrovDifferentiability.mem_directionalSliceQuotientEstimateSet_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} : x ∈ directionalSliceQuotientEstimateSet D v (u ∘ ⇑e) ↔ e x ∈ directionalSliceQuotientEstimateSet D (fun (i : ι) => e (v i)) u

Pointwise transport of finite directional quotient slice-good data through a linear isometry equivalence.

theorem AleksandrovDifferentiability.directionalSliceQuotientEstimateAt_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} : DirectionalSliceQuotientEstimateAt D v (u ∘ ⇑e) x ↔ DirectionalSliceQuotientEstimateAt D (fun (i : ι) => e (v i)) u (e x)

Pointwise transport of finite directional quotient-slice data through a linear isometry equivalence.

theorem AleksandrovDifferentiability.directionalSliceQuotientEstimateSet_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 → ℝ) : directionalSliceQuotientEstimateSet D v (u ∘ ⇑e) = ⇑e ⁻¹' directionalSliceQuotientEstimateSet D (fun (i : ι) => e (v i)) u

Set-level transport of finite directional quotient slice-good data through a linear isometry equivalence.

theorem AleksandrovDifferentiability.compatibleDirectionalSliceEstimateAt_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} : CompatibleDirectionalSliceEstimateAt D v (u ∘ ⇑e) x ↔ CompatibleDirectionalSliceEstimateAt D (fun (i : ι) => e (v i)) u (e x)

Pointwise transport of compatible finite directional slice data through a linear isometry equivalence. The common ambient slope is transported by the isometry.

theorem AleksandrovDifferentiability.compatibleDirectionalSliceEstimateSet_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 → ℝ) : compatibleDirectionalSliceEstimateSet D v (u ∘ ⇑e) = ⇑e ⁻¹' compatibleDirectionalSliceEstimateSet D (fun (i : ι) => e (v i)) u

Set-level transport of compatible finite directional slice data through a linear isometry equivalence.

theorem AleksandrovDifferentiability.symmetricCompatibleDirectionalSliceEstimateAt_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} : SymmetricCompatibleDirectionalSliceEstimateAt D v (u ∘ ⇑e) x ↔ SymmetricCompatibleDirectionalSliceEstimateAt D (fun (i : ι) => e (v i)) u (e x)

Pointwise transport of symmetric-compatible finite directional slice data through a linear isometry equivalence.

theorem AleksandrovDifferentiability.symmetricCompatibleDirectionalSliceEstimateSet_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 → ℝ) : symmetricCompatibleDirectionalSliceEstimateSet D v (u ∘ ⇑e) = ⇑e ⁻¹' symmetricCompatibleDirectionalSliceEstimateSet D (fun (i : ι) => e (v i)) u

Set-level transport of symmetric-compatible finite directional slice data through a linear isometry equivalence.

theorem AleksandrovDifferentiability.compatibleDirectionalSliceQuotientEstimateAt_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} : CompatibleDirectionalSliceQuotientEstimateAt D v (u ∘ ⇑e) x ↔ CompatibleDirectionalSliceQuotientEstimateAt D (fun (i : ι) => e (v i)) u (e x)

Pointwise transport of compatible finite quotient-slice data through a linear isometry equivalence.

theorem AleksandrovDifferentiability.compatibleDirectionalSliceQuotientEstimateSet_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 → ℝ) : compatibleDirectionalSliceQuotientEstimateSet D v (u ∘ ⇑e) = ⇑e ⁻¹' compatibleDirectionalSliceQuotientEstimateSet D (fun (i : ι) => e (v i)) u

Set-level transport of compatible finite quotient-slice data through a linear isometry equivalence.

theorem AleksandrovDifferentiability.symmetricCompatibleDirectionalSliceQuotientEstimateAt_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} : SymmetricCompatibleDirectionalSliceQuotientEstimateAt D v (u ∘ ⇑e) x ↔ SymmetricCompatibleDirectionalSliceQuotientEstimateAt D (fun (i : ι) => e (v i)) u (e x)

Pointwise transport of symmetric-compatible finite quotient-slice data through a linear isometry equivalence.

theorem AleksandrovDifferentiability.symmetricCompatibleDirectionalSliceQuotientEstimateSet_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 → ℝ) : symmetricCompatibleDirectionalSliceQuotientEstimateSet D v (u ∘ ⇑e) = ⇑e ⁻¹' symmetricCompatibleDirectionalSliceQuotientEstimateSet D (fun (i : ι) => e (v i)) u

Set-level transport of symmetric-compatible finite quotient-slice data through a linear isometry equivalence.