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

Scalar estimates along affine lines

This file records zero-direction cases and transport wrappers for scalar quadratic estimates on line restrictions.

theorem AleksandrovDifferentiability.mem_directionalLineScalarEstimateSet_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ) (x : E) : x ∈ directionalLineScalarEstimateSet 0 u

Every point is good for the zero-direction scalar estimate set.

theorem AleksandrovDifferentiability.mem_directionalLineScalarQuotientEstimateSet_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ) (x : E) : x ∈ directionalLineScalarQuotientEstimateSet 0 u

Every point is good for the zero-direction scalar quotient-estimate set.

@[simp]

theorem AleksandrovDifferentiability.directionalLineScalarEstimateSet_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ) : directionalLineScalarEstimateSet 0 u = Set.univ

@[simp]

theorem AleksandrovDifferentiability.directionalLineScalarQuotientEstimateSet_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ) : directionalLineScalarQuotientEstimateSet 0 u = Set.univ

theorem AleksandrovDifferentiability.mem_directionalLineScalarEstimateSet_inner_add_const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p v : E) (c : ℝ) (x : E) : x ∈ directionalLineScalarEstimateSet v fun (y : E) => inner ℝ p y + c

Affine ambient functions have scalar line-estimate data in every direction and at every base point.

theorem AleksandrovDifferentiability.mem_directionalLineScalarQuotientEstimateSet_inner_add_const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p v : E) (c : ℝ) (x : E) : x ∈ directionalLineScalarQuotientEstimateSet v fun (y : E) => inner ℝ p y + c

Quotient-estimate version of mem_directionalLineScalarEstimateSet_inner_add_const.

theorem AleksandrovDifferentiability.realScalarQuadraticEstimateWithDataAt_lineRestriction_inner_add_const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p x v : E) (c : ℝ) : RealScalarQuadraticEstimateWithDataAt (lineRestriction (fun (y : E) => inner ℝ p y + c) x v) 0 (inner ℝ p v) 0

Affine ambient functions have scalar line-estimate data with the ambient slope projected onto the line direction and zero quadratic coefficient.

theorem AleksandrovDifferentiability.realScalarQuadraticQuotientEstimateWithDataAt_lineRestriction_inner_add_const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p x v : E) (c : ℝ) : RealScalarQuadraticQuotientEstimateWithDataAt (lineRestriction (fun (y : E) => inner ℝ p y + c) x v) 0 (inner ℝ p v) 0

Quotient-estimate version of realScalarQuadraticEstimateWithDataAt_lineRestriction_inner_add_const.

theorem AleksandrovDifferentiability.directionalLineScalarEstimateSet_inner_add_const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p v : E) (c : ℝ) : (directionalLineScalarEstimateSet v fun (y : E) => inner ℝ p y + c) = Set.univ

For affine ambient functions, every point is good for every scalar directional-line estimate.

theorem AleksandrovDifferentiability.directionalLineScalarQuotientEstimateSet_inner_add_const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p v : E) (c : ℝ) : (directionalLineScalarQuotientEstimateSet v fun (y : E) => inner ℝ p y + c) = Set.univ

Quotient-estimate version of directionalLineScalarEstimateSet_inner_add_const.

theorem AleksandrovDifferentiability.compatibleDirectionalSliceEstimateAt_inner_add_const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (p : E) (c : ℝ) (x : E) : CompatibleDirectionalSliceEstimateAt D v (fun (y : E) => inner ℝ p y + c) x

Affine ambient functions carry compatible finite slice data for every finite direction list. The compatible ambient slope is the affine slope and all quadratic coefficients are zero.

theorem AleksandrovDifferentiability.symmetricCompatibleDirectionalSliceEstimateAt_inner_add_const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (p : E) (c : ℝ) (x : E) : SymmetricCompatibleDirectionalSliceEstimateAt D v (fun (y : E) => inner ℝ p y + c) x

Symmetric compatible finite slice data for affine ambient functions.

theorem AleksandrovDifferentiability.compatibleDirectionalSliceQuotientEstimateAt_inner_add_const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (p : E) (c : ℝ) (x : E) : CompatibleDirectionalSliceQuotientEstimateAt D v (fun (y : E) => inner ℝ p y + c) x

Quotient-estimate version of compatibleDirectionalSliceEstimateAt_inner_add_const.

theorem AleksandrovDifferentiability.symmetricCompatibleDirectionalSliceQuotientEstimateAt_inner_add_const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (p : E) (c : ℝ) (x : E) : SymmetricCompatibleDirectionalSliceQuotientEstimateAt D v (fun (y : E) => inner ℝ p y + c) x

Quotient-estimate version of symmetricCompatibleDirectionalSliceEstimateAt_inner_add_const.

theorem AleksandrovDifferentiability.compatibleDirectionalSliceEstimateSet_inner_add_const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (p : E) (c : ℝ) : (compatibleDirectionalSliceEstimateSet D v fun (y : E) => inner ℝ p y + c) = Set.univ

For affine ambient functions, every point carries compatible finite slice data.

theorem AleksandrovDifferentiability.symmetricCompatibleDirectionalSliceEstimateSet_inner_add_const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (p : E) (c : ℝ) : (symmetricCompatibleDirectionalSliceEstimateSet D v fun (y : E) => inner ℝ p y + c) = Set.univ

For affine ambient functions, every point carries symmetric compatible finite slice data.

theorem AleksandrovDifferentiability.compatibleDirectionalSliceQuotientEstimateSet_inner_add_const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (p : E) (c : ℝ) : (compatibleDirectionalSliceQuotientEstimateSet D v fun (y : E) => inner ℝ p y + c) = Set.univ

Quotient-estimate version of compatibleDirectionalSliceEstimateSet_inner_add_const.

theorem AleksandrovDifferentiability.symmetricCompatibleDirectionalSliceQuotientEstimateSet_inner_add_const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (p : E) (c : ℝ) : (symmetricCompatibleDirectionalSliceQuotientEstimateSet D v fun (y : E) => inner ℝ p y + c) = Set.univ

Quotient-estimate version of symmetricCompatibleDirectionalSliceEstimateSet_inner_add_const.

theorem AleksandrovDifferentiability.directionalLineScalarEstimateSet_smul_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : E} {c : ℝ} (hc : c ≠ 0) (u : E → ℝ) : directionalLineScalarEstimateSet (c • v) u = directionalLineScalarEstimateSet v u

Nonzero scalar rescaling of a direction does not change the scalar directional-line good set.

theorem AleksandrovDifferentiability.directionalLineScalarQuotientEstimateSet_smul_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : E} {c : ℝ} (hc : c ≠ 0) (u : E → ℝ) : directionalLineScalarQuotientEstimateSet (c • v) u = directionalLineScalarQuotientEstimateSet v u

Quotient-estimate version of directionalLineScalarEstimateSet_smul_eq.

@[simp]

theorem AleksandrovDifferentiability.directionalLineScalarEstimateSet_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : E) (u : E → ℝ) : directionalLineScalarEstimateSet (-v) u = directionalLineScalarEstimateSet v u

@[simp]

theorem AleksandrovDifferentiability.directionalLineScalarQuotientEstimateSet_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : E) (u : E → ℝ) : directionalLineScalarQuotientEstimateSet (-v) u = directionalLineScalarQuotientEstimateSet v u

theorem AleksandrovDifferentiability.directionalLineScalarEstimateSet_subset_directionalLineScalarQuotientEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : E} {u : E → ℝ} : directionalLineScalarEstimateSet v u ⊆ directionalLineScalarQuotientEstimateSet v u

The fixed-direction scalar estimate good set is contained in its punctured normalized quotient version.

theorem AleksandrovDifferentiability.RealScalarQuadraticEstimateAt.real_lineRestriction {f : ℝ → ℝ} {x ξ : ℝ} (h : RealScalarQuadraticEstimateAt f x) : RealScalarQuadraticEstimateAt (lineRestriction f x ξ) 0

On ℝ, scalar quadratic estimate data at a point gives scalar estimate data on the restriction to any real affine line through that point.

theorem AleksandrovDifferentiability.RealScalarQuadraticEstimateAt.of_real_lineRestriction_one {f : ℝ → ℝ} {x : ℝ} (h : RealScalarQuadraticEstimateAt (lineRestriction f x 1) 0) : RealScalarQuadraticEstimateAt f x

A scalar estimate for the unit real-line restriction through x is exactly a scalar estimate at x.

theorem AleksandrovDifferentiability.RealScalarQuadraticQuotientEstimateAt.real_lineRestriction {f : ℝ → ℝ} {x ξ : ℝ} (h : RealScalarQuadraticQuotientEstimateAt f x) : RealScalarQuadraticQuotientEstimateAt (lineRestriction f x ξ) 0

Quotient-estimate version of RealScalarQuadraticEstimateAt.real_lineRestriction.

theorem AleksandrovDifferentiability.RealScalarQuadraticQuotientEstimateAt.of_real_lineRestriction_one {f : ℝ → ℝ} {x : ℝ} (h : RealScalarQuadraticQuotientEstimateAt (lineRestriction f x 1) 0) : RealScalarQuadraticQuotientEstimateAt f x

Punctured normalized quotient version of RealScalarQuadraticEstimateAt.of_real_lineRestriction_one.

theorem AleksandrovDifferentiability.RealScalarQuadraticEstimateAt.compatibleDirectionalSliceEstimateAt_real {ι : Type u_2} {D : Finset ι} {v : ι → ℝ} {f : ℝ → ℝ} {x : ℝ} (h : RealScalarQuadraticEstimateAt f x) : CompatibleDirectionalSliceEstimateAt D v f x

On the real line, scalar quadratic estimate data at a point supplies compatible finite slice data for any finite family of real directions: every line slope is obtained from the same ambient scalar first-order coefficient.

theorem AleksandrovDifferentiability.RealScalarQuadraticQuotientEstimateAt.compatibleDirectionalSliceQuotientEstimateAt_real {ι : Type u_2} {D : Finset ι} {v : ι → ℝ} {f : ℝ → ℝ} {x : ℝ} (h : RealScalarQuadraticQuotientEstimateAt f x) : CompatibleDirectionalSliceQuotientEstimateAt D v f x

Punctured normalized quotient version of RealScalarQuadraticEstimateAt.compatibleDirectionalSliceEstimateAt_real.

theorem AleksandrovDifferentiability.realScalarQuadraticEstimateSet_subset_directionalLineScalarEstimateSet (ξ : ℝ) (f : ℝ → ℝ) : realScalarQuadraticEstimateSet f ⊆ directionalLineScalarEstimateSet ξ f

On the real line, the ordinary scalar-estimate good set is contained in every directional line scalar-estimate good set.

theorem AleksandrovDifferentiability.realScalarQuadraticQuotientEstimateSet_subset_directionalLineScalarQuotientEstimateSet (ξ : ℝ) (f : ℝ → ℝ) : realScalarQuadraticQuotientEstimateSet f ⊆ directionalLineScalarQuotientEstimateSet ξ f

Quotient-estimate version of realScalarQuadraticEstimateSet_subset_directionalLineScalarEstimateSet.

theorem AleksandrovDifferentiability.norm_inv_norm_smul_eq_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {w : E} (hw : w ≠ 0) : ‖‖w‖⁻¹ • w‖ = 1

Normalizing a nonzero direction by the inverse of its norm gives a unit direction.