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

Real scalar quadratic estimates

One-dimensional scalar quadratic estimate predicates and transport lemmas.

theorem AleksandrovDifferentiability.hasSecondOrderExpansionAt_real_of_eventually_norm_sub_quadratic_le_mul {f : ℝ → ℝ} {x p q : ℝ} (h : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (z : ℝ) in nhds 0, ‖f (x + z) - f x - p * z - 1 / 2 * q * z ^ 2‖ ≤ ε * ‖z‖ ^ 2) : HasSecondOrderExpansionAt f x p (q • 1)

Real-line scalar form of the local quadratic estimate-to-expansion constructor. This is the shape expected from one-dimensional estimates: the Hessian candidate is the scalar q, encoded as q times the identity operator on ℝ.

theorem AleksandrovDifferentiability.hasSecondOrderExpansionAt_real_of_eventually_norm_sub_quadratic_div_norm_sq_le {f : ℝ → ℝ} {x p q : ℝ} (h : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (z : ℝ) in nhdsWithin 0 {z : ℝ | z ≠ 0}, ‖f (x + z) - f x - p * z - 1 / 2 * q * z ^ 2‖ / ‖z‖ ^ 2 ≤ ε) : HasSecondOrderExpansionAt f x p (q • 1)

Real-line scalar form of the punctured normalized quadratic estimate-to-expansion constructor.

theorem AleksandrovDifferentiability.secondOrderDifferentiableAt_real_of_eventually_norm_sub_quadratic_le_mul {f : ℝ → ℝ} {x p q : ℝ} (h : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (z : ℝ) in nhds 0, ‖f (x + z) - f x - p * z - 1 / 2 * q * z ^ 2‖ ≤ ε * ‖z‖ ^ 2) : SecondOrderDifferentiableAt f x

Real-line scalar form of the local quadratic estimate-to-second-order-differentiability constructor.

theorem AleksandrovDifferentiability.secondOrderDifferentiableAt_real_of_eventually_norm_sub_quadratic_div_norm_sq_le {f : ℝ → ℝ} {x p q : ℝ} (h : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (z : ℝ) in nhdsWithin 0 {z : ℝ | z ≠ 0}, ‖f (x + z) - f x - p * z - 1 / 2 * q * z ^ 2‖ / ‖z‖ ^ 2 ≤ ε) : SecondOrderDifferentiableAt f x

Real-line scalar form of the punctured normalized quadratic estimate-to-second-order-differentiability constructor.

def AleksandrovDifferentiability.RealScalarQuadraticEstimateAt (f : ℝ → ℝ) (x : ℝ) : Prop

Pointwise real-line scalar quadratic estimate data. This names the usual one-dimensional target estimate before it is converted into the project second-order expansion predicate.

Equations

• AleksandrovDifferentiability.RealScalarQuadraticEstimateAt f x = ∃ (p : ℝ) (q : ℝ), ∀ (ε : ℝ), 0 < ε → ∀ᶠ (z : ℝ) in nhds 0, ‖f (x + z) - f x - p * z - 1 / 2 * q * z ^ 2‖ ≤ ε * ‖z‖ ^ 2

def AleksandrovDifferentiability.RealScalarQuadraticEstimateWithDataAt (f : ℝ → ℝ) (x p q : ℝ) : Prop

Real-line scalar quadratic estimate data with the first-order and quadratic coefficients specified explicitly. This is useful when several line estimates must share coefficients coming from one ambient affine slope.

Equations

• AleksandrovDifferentiability.RealScalarQuadraticEstimateWithDataAt f x p q = ∀ (ε : ℝ), 0 < ε → ∀ᶠ (z : ℝ) in nhds 0, ‖f (x + z) - f x - p * z - 1 / 2 * q * z ^ 2‖ ≤ ε * ‖z‖ ^ 2

def AleksandrovDifferentiability.RealScalarQuadraticQuotientEstimateAt (f : ℝ → ℝ) (x : ℝ) : Prop

Punctured normalized quotient version of RealScalarQuadraticEstimateAt.

Equations

• One or more equations did not get rendered due to their size.

def AleksandrovDifferentiability.RealScalarQuadraticQuotientEstimateWithDataAt (f : ℝ → ℝ) (x p q : ℝ) : Prop

Punctured normalized scalar quadratic quotient estimate with explicit coefficients.

Equations

• One or more equations did not get rendered due to their size.

theorem AleksandrovDifferentiability.RealScalarQuadraticEstimateWithDataAt.realScalarQuadraticEstimateAt {f : ℝ → ℝ} {x p q : ℝ} (h : RealScalarQuadraticEstimateWithDataAt f x p q) : RealScalarQuadraticEstimateAt f x

Explicit scalar estimate data implies the existential scalar estimate predicate.

theorem AleksandrovDifferentiability.RealScalarQuadraticQuotientEstimateWithDataAt.realScalarQuadraticQuotientEstimateAt {f : ℝ → ℝ} {x p q : ℝ} (h : RealScalarQuadraticQuotientEstimateWithDataAt f x p q) : RealScalarQuadraticQuotientEstimateAt f x

Explicit scalar quotient-estimate data implies the existential scalar quotient predicate.

theorem AleksandrovDifferentiability.RealScalarQuadraticEstimateWithDataAt.quadraticQuotientEstimateWithDataAt {f : ℝ → ℝ} {x p q : ℝ} (h : RealScalarQuadraticEstimateWithDataAt f x p q) : RealScalarQuadraticQuotientEstimateWithDataAt f x p q

Explicit scalar estimate data gives the explicit punctured normalized quotient estimate with the same coefficients.

theorem AleksandrovDifferentiability.RealScalarQuadraticEstimateWithDataAt.average {f : ℝ → ℝ} {x p q q' : ℝ} (hq : RealScalarQuadraticEstimateWithDataAt f x p q) (hq' : RealScalarQuadraticEstimateWithDataAt f x p q') : RealScalarQuadraticEstimateWithDataAt f x p ((q + q') / 2)

Two scalar quadratic estimates with the same base point and first-order coefficient can be averaged in their quadratic coefficient.

theorem AleksandrovDifferentiability.RealScalarQuadraticQuotientEstimateWithDataAt.average {f : ℝ → ℝ} {x p q q' : ℝ} (hq : RealScalarQuadraticQuotientEstimateWithDataAt f x p q) (hq' : RealScalarQuadraticQuotientEstimateWithDataAt f x p q') : RealScalarQuadraticQuotientEstimateWithDataAt f x p ((q + q') / 2)

Quotient-form scalar estimates with the same base point and first-order coefficient can be averaged in their quadratic coefficient.

theorem AleksandrovDifferentiability.RealScalarQuadraticEstimateWithDataAt.comp_mul {f : ℝ → ℝ} {p q c : ℝ} (h : RealScalarQuadraticEstimateWithDataAt f 0 p q) : RealScalarQuadraticEstimateWithDataAt (fun (t : ℝ) => f (c * t)) 0 (c * p) (c ^ 2 * q)

Scalar quadratic estimates are stable under rescaling the line parameter. This is the coefficient bookkeeping behind replacing a line direction v by c • v.

theorem AleksandrovDifferentiability.RealScalarQuadraticQuotientEstimateWithDataAt.comp_mul {f : ℝ → ℝ} {p q c : ℝ} (h : RealScalarQuadraticQuotientEstimateWithDataAt f 0 p q) : RealScalarQuadraticQuotientEstimateWithDataAt (fun (t : ℝ) => f (c * t)) 0 (c * p) (c ^ 2 * q)

Quotient-form scalar estimates are stable under rescaling the line parameter.

theorem AleksandrovDifferentiability.RealScalarQuadraticEstimateWithDataAt.recenter_zero {f : ℝ → ℝ} {x p q : ℝ} (h : RealScalarQuadraticEstimateWithDataAt f x p q) : RealScalarQuadraticEstimateWithDataAt (fun (z : ℝ) => f (x + z)) 0 p q

Recenter scalar quadratic estimate data at x as estimate data at 0 for the translated function z ↦ f (x + z).

theorem AleksandrovDifferentiability.RealScalarQuadraticQuotientEstimateWithDataAt.recenter_zero {f : ℝ → ℝ} {x p q : ℝ} (h : RealScalarQuadraticQuotientEstimateWithDataAt f x p q) : RealScalarQuadraticQuotientEstimateWithDataAt (fun (z : ℝ) => f (x + z)) 0 p q

Quotient-estimate version of RealScalarQuadraticEstimateWithDataAt.recenter_zero.

theorem AleksandrovDifferentiability.RealScalarQuadraticEstimateWithDataAt.real_lineRestriction {f : ℝ → ℝ} {x ξ p q : ℝ} (h : RealScalarQuadraticEstimateWithDataAt f x p q) : RealScalarQuadraticEstimateWithDataAt (lineRestriction f x ξ) 0 (ξ * p) (ξ ^ 2 * q)

On the real line, scalar quadratic estimate data at x transfers to the restriction of f to the affine line through x with real direction ξ.

theorem AleksandrovDifferentiability.RealScalarQuadraticQuotientEstimateWithDataAt.real_lineRestriction {f : ℝ → ℝ} {x ξ p q : ℝ} (h : RealScalarQuadraticQuotientEstimateWithDataAt f x p q) : RealScalarQuadraticQuotientEstimateWithDataAt (lineRestriction f x ξ) 0 (ξ * p) (ξ ^ 2 * q)

Quotient-estimate version of RealScalarQuadraticEstimateWithDataAt.real_lineRestriction.

theorem AleksandrovDifferentiability.RealScalarQuadraticEstimateWithDataAt.lineRestriction_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} {p q c : ℝ} (h : RealScalarQuadraticEstimateWithDataAt (lineRestriction u x v) 0 p q) : RealScalarQuadraticEstimateWithDataAt (lineRestriction u x (c • v)) 0 (c * p) (c ^ 2 * q)

Line-restriction version of RealScalarQuadraticEstimateWithDataAt.comp_mul: replacing the direction v by c • v scales the first coefficient by c and the quadratic coefficient by c ^ 2.

theorem AleksandrovDifferentiability.RealScalarQuadraticQuotientEstimateWithDataAt.lineRestriction_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} {p q c : ℝ} (h : RealScalarQuadraticQuotientEstimateWithDataAt (lineRestriction u x v) 0 p q) : RealScalarQuadraticQuotientEstimateWithDataAt (lineRestriction u x (c • v)) 0 (c * p) (c ^ 2 * q)

Quotient-estimate version of RealScalarQuadraticEstimateWithDataAt.lineRestriction_smul.

theorem AleksandrovDifferentiability.RealScalarQuadraticEstimateWithDataAt.lineRestriction_add_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p v : E} {q : ℝ} (h : RealScalarQuadraticEstimateWithDataAt (lineRestriction u x v) 0 (inner ℝ p v) q) : RealScalarQuadraticEstimateWithDataAt (lineRestriction u x (v + v)) 0 (inner ℝ p (v + v)) (4 * q)

Diagonal pair-direction version of line-restriction rescaling: the direction v + v carries the first-order coefficient from the ambient slope and the quadratic coefficient 4 * q.

theorem AleksandrovDifferentiability.RealScalarQuadraticQuotientEstimateWithDataAt.lineRestriction_add_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x p v : E} {q : ℝ} (h : RealScalarQuadraticQuotientEstimateWithDataAt (lineRestriction u x v) 0 (inner ℝ p v) q) : RealScalarQuadraticQuotientEstimateWithDataAt (lineRestriction u x (v + v)) 0 (inner ℝ p (v + v)) (4 * q)

Quotient-estimate version of RealScalarQuadraticEstimateWithDataAt.lineRestriction_add_self.

theorem AleksandrovDifferentiability.RealScalarQuadraticEstimateAt.lineRestriction_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} {c : ℝ} (h : RealScalarQuadraticEstimateAt (lineRestriction u x v) 0) : RealScalarQuadraticEstimateAt (lineRestriction u x (c • v)) 0

Existential scalar estimate version of line-restriction rescaling.

theorem AleksandrovDifferentiability.RealScalarQuadraticQuotientEstimateAt.lineRestriction_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} {c : ℝ} (h : RealScalarQuadraticQuotientEstimateAt (lineRestriction u x v) 0) : RealScalarQuadraticQuotientEstimateAt (lineRestriction u x (c • v)) 0

Existential scalar quotient-estimate version of line-restriction rescaling.

theorem AleksandrovDifferentiability.RealScalarQuadraticEstimateAt.lineRestriction_smul_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} {c : ℝ} (hc : c ≠ 0) : RealScalarQuadraticEstimateAt (lineRestriction u x (c • v)) 0 ↔ RealScalarQuadraticEstimateAt (lineRestriction u x v) 0

Nonzero rescaling of a line direction preserves the existential scalar estimate predicate.

theorem AleksandrovDifferentiability.RealScalarQuadraticQuotientEstimateAt.lineRestriction_smul_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} {c : ℝ} (hc : c ≠ 0) : RealScalarQuadraticQuotientEstimateAt (lineRestriction u x (c • v)) 0 ↔ RealScalarQuadraticQuotientEstimateAt (lineRestriction u x v) 0

Quotient-estimate version of RealScalarQuadraticEstimateAt.lineRestriction_smul_iff.

theorem AleksandrovDifferentiability.RealScalarQuadraticEstimateAt.lineRestriction_add_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} (h : RealScalarQuadraticEstimateAt (lineRestriction u x v) 0) : RealScalarQuadraticEstimateAt (lineRestriction u x (v + v)) 0

Existential scalar estimate version for the diagonal pair direction v + v.

theorem AleksandrovDifferentiability.RealScalarQuadraticQuotientEstimateAt.lineRestriction_add_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} (h : RealScalarQuadraticQuotientEstimateAt (lineRestriction u x v) 0) : RealScalarQuadraticQuotientEstimateAt (lineRestriction u x (v + v)) 0

Existential scalar quotient-estimate version for the diagonal pair direction v + v.

theorem AleksandrovDifferentiability.realScalarQuadraticEstimateWithDataAt_const (c x : ℝ) : RealScalarQuadraticEstimateWithDataAt (fun (x : ℝ) => c) x 0 0

Constant real-line functions have scalar quadratic estimate data with zero coefficients.

theorem AleksandrovDifferentiability.realScalarQuadraticQuotientEstimateWithDataAt_const (c x : ℝ) : RealScalarQuadraticQuotientEstimateWithDataAt (fun (x : ℝ) => c) x 0 0

Constant real-line functions have punctured scalar quotient-estimate data with zero coefficients.

theorem AleksandrovDifferentiability.realScalarQuadraticEstimateAt_const (c x : ℝ) : RealScalarQuadraticEstimateAt (fun (x : ℝ) => c) x

Existential scalar estimate form for constant real-line functions.

theorem AleksandrovDifferentiability.realScalarQuadraticQuotientEstimateAt_const (c x : ℝ) : RealScalarQuadraticQuotientEstimateAt (fun (x : ℝ) => c) x

Existential quotient-estimate form for constant real-line functions.

theorem AleksandrovDifferentiability.realScalarQuadraticEstimateWithDataAt_affine (a b x : ℝ) : RealScalarQuadraticEstimateWithDataAt (fun (t : ℝ) => a * t + b) x a 0

Real affine functions have scalar quadratic estimate data with zero quadratic coefficient.

theorem AleksandrovDifferentiability.realScalarQuadraticQuotientEstimateWithDataAt_affine (a b x : ℝ) : RealScalarQuadraticQuotientEstimateWithDataAt (fun (t : ℝ) => a * t + b) x a 0

Punctured normalized quotient-estimate version of realScalarQuadraticEstimateWithDataAt_affine.

theorem AleksandrovDifferentiability.realScalarQuadraticEstimateAt_affine (a b x : ℝ) : RealScalarQuadraticEstimateAt (fun (t : ℝ) => a * t + b) x

Existential scalar estimate form for real affine functions.

theorem AleksandrovDifferentiability.realScalarQuadraticQuotientEstimateAt_affine (a b x : ℝ) : RealScalarQuadraticQuotientEstimateAt (fun (t : ℝ) => a * t + b) x

Existential quotient-estimate form for real affine functions.

theorem AleksandrovDifferentiability.realScalarQuadraticEstimateAt_lineRestriction_zero_direction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ) (x : E) : RealScalarQuadraticEstimateAt (lineRestriction u x 0) 0

A zero-direction line restriction has scalar quadratic estimate data at the base parameter.

theorem AleksandrovDifferentiability.realScalarQuadraticQuotientEstimateAt_lineRestriction_zero_direction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ) (x : E) : RealScalarQuadraticQuotientEstimateAt (lineRestriction u x 0) 0

Quotient-estimate version of realScalarQuadraticEstimateAt_lineRestriction_zero_direction.

theorem AleksandrovDifferentiability.RealScalarQuadraticEstimateWithDataAt.lineRestriction_rebase {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} {t p q : ℝ} (h : RealScalarQuadraticEstimateWithDataAt (lineRestriction u x v) t p q) : RealScalarQuadraticEstimateWithDataAt (lineRestriction u (x + t • v) v) 0 p q

Rebase scalar estimate data from a parameter t on the line through x to parameter 0 on the same geometric line based at x + t • v.

theorem AleksandrovDifferentiability.RealScalarQuadraticQuotientEstimateWithDataAt.lineRestriction_rebase {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} {t p q : ℝ} (h : RealScalarQuadraticQuotientEstimateWithDataAt (lineRestriction u x v) t p q) : RealScalarQuadraticQuotientEstimateWithDataAt (lineRestriction u (x + t • v) v) 0 p q

Quotient-estimate version of RealScalarQuadraticEstimateWithDataAt.lineRestriction_rebase.

theorem AleksandrovDifferentiability.RealScalarQuadraticEstimateAt.lineRestriction_rebase {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} {t : ℝ} (h : RealScalarQuadraticEstimateAt (lineRestriction u x v) t) : RealScalarQuadraticEstimateAt (lineRestriction u (x + t • v) v) 0

Existential scalar estimate rebase from a line parameter to the corresponding ambient base point on the same line.

theorem AleksandrovDifferentiability.RealScalarQuadraticQuotientEstimateAt.lineRestriction_rebase {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x v : E} {t : ℝ} (h : RealScalarQuadraticQuotientEstimateAt (lineRestriction u x v) t) : RealScalarQuadraticQuotientEstimateAt (lineRestriction u (x + t • v) v) 0

Quotient-estimate existential rebase from a line parameter to the corresponding ambient base point on the same line.

theorem AleksandrovDifferentiability.realScalarQuadraticEstimateWithDataAt_of_hasSecondOrderExpansionAt {f : ℝ → ℝ} {x p : ℝ} {B : ℝ →L[ℝ] ℝ} (h : HasSecondOrderExpansionAt f x p B) : RealScalarQuadraticEstimateWithDataAt f x p (B 1)

On the real line, a project-level second-order expansion gives the scalar quadratic estimate shape used by the one-dimensional assembly interface.

theorem AleksandrovDifferentiability.realScalarQuadraticEstimateAt_of_hasSecondOrderExpansionAt {f : ℝ → ℝ} {x p : ℝ} {B : ℝ →L[ℝ] ℝ} (h : HasSecondOrderExpansionAt f x p B) : RealScalarQuadraticEstimateAt f x

On the real line, a project-level second-order expansion gives the scalar quadratic estimate shape used by the one-dimensional assembly interface.

theorem AleksandrovDifferentiability.realScalarQuadraticEstimateAt_of_secondOrderDifferentiableAt {f : ℝ → ℝ} {x : ℝ} (h : SecondOrderDifferentiableAt f x) : RealScalarQuadraticEstimateAt f x

On the real line, project-level second-order differentiability gives the scalar quadratic estimate shape used by the one-dimensional assembly interface.

theorem AleksandrovDifferentiability.realScalarQuadraticEstimateAt_of_rightDeriv_averageRemainder_of_hasDerivWithinAt {S : Set ℝ} {f : ℝ → ℝ} {x q : ℝ} (hx : x ∈ interior S) (havg : HasRightDerivAverageRemainderAt f x) (hderiv : HasDerivWithinAt (rightDeriv f) q (interior S) x) : RealScalarQuadraticEstimateAt f x

The averaged right-derivative remainder estimate, together with differentiability of the right derivative, gives the project's scalar quadratic estimate.

This theorem isolates the remaining genuinely one-dimensional convex analytic ingredient: for convex functions, one still has to prove HasRightDerivAverageRemainderAt at the derivative-good points. Once that averaging estimate is available, the passage to the usual (1 / 2) * q * z ^ 2 Taylor coefficient is formal.

theorem AleksandrovDifferentiability.realScalarQuadraticEstimateAt_of_mem_oneSidedDerivDifferentiabilitySet_of_averageRemainder {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hx : x ∈ interior S) (hgood : x ∈ oneSidedDerivDifferentiabilitySet S f) (havg : HasRightDerivAverageRemainderAt f x) : RealScalarQuadraticEstimateAt f x

Derivative-good points satisfy the scalar quadratic estimate once the averaged right-derivative remainder estimate is known there.

theorem AleksandrovDifferentiability.realScalarQuadraticEstimateAt_of_taylor_isLittleO {f : ℝ → ℝ} {x p q : ℝ} (h : (fun (y : ℝ) => f y - (f x + p * (y - x) + 1 / 2 * q * (y - x) ^ 2)) =o[nhds x] fun (y : ℝ) => (y - x) ^ 2) : RealScalarQuadraticEstimateAt f x

A usual scalar Taylor little-o expansion gives the project-local scalar quadratic estimate at the base point.

theorem AleksandrovDifferentiability.realScalarQuadraticEstimateAt_of_contDiffOn_two_of_mem_interior {s : Set ℝ} {f : ℝ → ℝ} {x : ℝ} (hs : Convex ℝ s) (hx : x ∈ interior s) (hf : ContDiffOn ℝ 2 f s) : RealScalarQuadraticEstimateAt f x

A C^2 real function on a convex neighborhood of x satisfies the project-local scalar quadratic estimate at x. This is a direct wrapper around Mathlib's Taylor theorem, with the Taylor polynomial coefficients exposed in the project's scalar-estimate format.

def AleksandrovDifferentiability.realScalarQuadraticEstimateSet (f : ℝ → ℝ) : Set ℝ

Points carrying real-line scalar quadratic estimate data.

Equations

• AleksandrovDifferentiability.realScalarQuadraticEstimateSet f = {x : ℝ | AleksandrovDifferentiability.RealScalarQuadraticEstimateAt f x}

def AleksandrovDifferentiability.realScalarQuadraticQuotientEstimateSet (f : ℝ → ℝ) : Set ℝ

Points carrying punctured normalized real-line scalar quadratic estimate data.

Equations

• AleksandrovDifferentiability.realScalarQuadraticQuotientEstimateSet f = {x : ℝ | AleksandrovDifferentiability.RealScalarQuadraticQuotientEstimateAt f x}

@[simp]

theorem AleksandrovDifferentiability.mem_realScalarQuadraticEstimateSet {f : ℝ → ℝ} {x : ℝ} : x ∈ realScalarQuadraticEstimateSet f ↔ RealScalarQuadraticEstimateAt f x

@[simp]

theorem AleksandrovDifferentiability.mem_realScalarQuadraticQuotientEstimateSet {f : ℝ → ℝ} {x : ℝ} : x ∈ realScalarQuadraticQuotientEstimateSet f ↔ RealScalarQuadraticQuotientEstimateAt f x

theorem AleksandrovDifferentiability.RealScalarQuadraticEstimateAt.secondOrderDifferentiableAt {f : ℝ → ℝ} {x : ℝ} (h : RealScalarQuadraticEstimateAt f x) : SecondOrderDifferentiableAt f x

Scalar quadratic estimate data implies project second-order differentiability on ℝ.

theorem AleksandrovDifferentiability.RealScalarQuadraticQuotientEstimateAt.secondOrderDifferentiableAt {f : ℝ → ℝ} {x : ℝ} (h : RealScalarQuadraticQuotientEstimateAt f x) : SecondOrderDifferentiableAt f x

Scalar quotient-estimate data implies project second-order differentiability on ℝ.

theorem AleksandrovDifferentiability.RealScalarQuadraticEstimateAt.quadraticQuotientEstimateAt {f : ℝ → ℝ} {x : ℝ} (h : RealScalarQuadraticEstimateAt f x) : RealScalarQuadraticQuotientEstimateAt f x

A local real-line scalar quadratic estimate implies the punctured normalized quotient estimate.

theorem AleksandrovDifferentiability.realScalarQuadraticEstimateSet_subset_secondOrderDifferentiabilitySet {f : ℝ → ℝ} : realScalarQuadraticEstimateSet f ⊆ secondOrderDifferentiabilitySet f

The scalar estimate good set is contained in the second-order differentiability locus.

theorem AleksandrovDifferentiability.realScalarQuadraticQuotientEstimateSet_subset_secondOrderDifferentiabilitySet {f : ℝ → ℝ} : realScalarQuadraticQuotientEstimateSet f ⊆ secondOrderDifferentiabilitySet f

The scalar quotient-estimate good set is contained in the second-order differentiability locus.

theorem AleksandrovDifferentiability.realScalarQuadraticEstimateSet_subset_realScalarQuadraticQuotientEstimateSet {f : ℝ → ℝ} : realScalarQuadraticEstimateSet f ⊆ realScalarQuadraticQuotientEstimateSet f

The local scalar estimate set is contained in the scalar quotient-estimate set.