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

Assembly from directional quadratic estimates

This file specializes the project estimate-assembly lemmas to Hessian candidates reconstructed from finitely many directional coefficients. It is a small bridge between future slicing data and the existing SecondOrderDifferentiableAEOn interface.

def AleksandrovDifferentiability.MixedDirectionalQuadraticEstimateAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (u : E → ℝ) (x : E) : Prop

Pointwise local quadratic estimate data whose Hessian candidate is assembled from a finite matrix of directional coefficients.

Equations

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

def AleksandrovDifferentiability.MixedDirectionalQuadraticQuotientEstimateAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (u : E → ℝ) (x : E) : Prop

Punctured normalized quotient version of MixedDirectionalQuadraticEstimateAt.

Equations

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

def AleksandrovDifferentiability.PolarizedMixedDirectionalQuadraticEstimateAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] (D : Finset ι) (v : ι → E) (u : E → ℝ) (x : E) : Prop

Pointwise local quadratic estimate data whose Hessian candidate is assembled from pure directional coefficients q i and pairwise-sum coefficients r i j by polarization. This is a closer target for the later finite slicing reconstruction than an arbitrary coefficient matrix.

Equations

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

def AleksandrovDifferentiability.PolarizedMixedDirectionalQuadraticQuotientEstimateAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] (D : Finset ι) (v : ι → E) (u : E → ℝ) (x : E) : Prop

Punctured normalized quotient version of PolarizedMixedDirectionalQuadraticEstimateAt.

Equations

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

def AleksandrovDifferentiability.DirectionalSliceEstimateAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (u : E → ℝ) (x : E) : Prop

Pointwise finite slicing target: scalar quadratic estimate data holds for the line restriction in each selected direction and each pairwise sum direction. This is the finite direction list needed by polarization-based Hessian reconstruction.

Equations

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

def AleksandrovDifferentiability.CompatibleDirectionalSliceEstimateAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (u : E → ℝ) (x : E) : Prop

Finite slicing target with compatible first-order data: all selected line estimates use the directional slopes coming from one ambient vector p. The coefficients q and r are the pure and pairwise-sum quadratic coefficients used by the polarization reconstruction.

Equations

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

def AleksandrovDifferentiability.SymmetricCompatibleDirectionalSliceEstimateAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (u : E → ℝ) (x : E) : Prop

Compatible finite slicing data with pairwise-sum coefficients symmetric on the selected finite direction set. This is the coefficient shape expected by the polarized reconstruction algebra.

Equations

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

def AleksandrovDifferentiability.DirectionalSliceQuotientEstimateAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (u : E → ℝ) (x : E) : Prop

Punctured normalized quotient version of DirectionalSliceEstimateAt.

Equations

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

def AleksandrovDifferentiability.CompatibleDirectionalSliceQuotientEstimateAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (u : E → ℝ) (x : E) : Prop

Punctured normalized quotient version of CompatibleDirectionalSliceEstimateAt.

Equations

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

def AleksandrovDifferentiability.SymmetricCompatibleDirectionalSliceQuotientEstimateAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (u : E → ℝ) (x : E) : Prop

Punctured normalized quotient version of SymmetricCompatibleDirectionalSliceEstimateAt.

Equations

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

def AleksandrovDifferentiability.mixedDirectionalQuadraticEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (u : E → ℝ) : Set E

Points carrying mixed-directional quadratic estimate data.

Equations

• AleksandrovDifferentiability.mixedDirectionalQuadraticEstimateSet D v u = {x : E | AleksandrovDifferentiability.MixedDirectionalQuadraticEstimateAt D v u x}

def AleksandrovDifferentiability.mixedDirectionalQuadraticQuotientEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (u : E → ℝ) : Set E

Points carrying punctured normalized mixed-directional quadratic estimate data.

Equations

• AleksandrovDifferentiability.mixedDirectionalQuadraticQuotientEstimateSet D v u = {x : E | AleksandrovDifferentiability.MixedDirectionalQuadraticQuotientEstimateAt D v u x}

def AleksandrovDifferentiability.polarizedMixedDirectionalQuadraticEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] (D : Finset ι) (v : ι → E) (u : E → ℝ) : Set E

Points carrying polarized mixed-directional quadratic estimate data.

Equations

• AleksandrovDifferentiability.polarizedMixedDirectionalQuadraticEstimateSet D v u = {x : E | AleksandrovDifferentiability.PolarizedMixedDirectionalQuadraticEstimateAt D v u x}

def AleksandrovDifferentiability.polarizedMixedDirectionalQuadraticQuotientEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] (D : Finset ι) (v : ι → E) (u : E → ℝ) : Set E

Points carrying punctured normalized polarized mixed-directional quadratic estimate data.

Equations

• AleksandrovDifferentiability.polarizedMixedDirectionalQuadraticQuotientEstimateSet D v u = {x : E | AleksandrovDifferentiability.PolarizedMixedDirectionalQuadraticQuotientEstimateAt D v u x}

def AleksandrovDifferentiability.directionalSliceEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (u : E → ℝ) : Set E

Points carrying scalar estimate data on the finite list of selected directions and their pairwise sums.

Equations

• AleksandrovDifferentiability.directionalSliceEstimateSet D v u = {x : E | AleksandrovDifferentiability.DirectionalSliceEstimateAt D v u x}

def AleksandrovDifferentiability.compatibleDirectionalSliceEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (u : E → ℝ) : Set E

Points carrying compatible scalar estimate data on the finite list of selected directions and their pairwise sums.

Equations

• AleksandrovDifferentiability.compatibleDirectionalSliceEstimateSet D v u = {x : E | AleksandrovDifferentiability.CompatibleDirectionalSliceEstimateAt D v u x}

def AleksandrovDifferentiability.symmetricCompatibleDirectionalSliceEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (u : E → ℝ) : Set E

Points carrying symmetric compatible scalar estimate data on the finite list of selected directions and their pairwise sums.

Equations

• AleksandrovDifferentiability.symmetricCompatibleDirectionalSliceEstimateSet D v u = {x : E | AleksandrovDifferentiability.SymmetricCompatibleDirectionalSliceEstimateAt D v u x}

def AleksandrovDifferentiability.directionalSliceQuotientEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (u : E → ℝ) : Set E

Points carrying scalar quotient-estimate data on the finite list of selected directions and their pairwise sums.

Equations

• AleksandrovDifferentiability.directionalSliceQuotientEstimateSet D v u = {x : E | AleksandrovDifferentiability.DirectionalSliceQuotientEstimateAt D v u x}

def AleksandrovDifferentiability.compatibleDirectionalSliceQuotientEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (u : E → ℝ) : Set E

Points carrying compatible scalar quotient-estimate data on the finite list of selected directions and their pairwise sums.

Equations

• AleksandrovDifferentiability.compatibleDirectionalSliceQuotientEstimateSet D v u = {x : E | AleksandrovDifferentiability.CompatibleDirectionalSliceQuotientEstimateAt D v u x}

def AleksandrovDifferentiability.symmetricCompatibleDirectionalSliceQuotientEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} (D : Finset ι) (v : ι → E) (u : E → ℝ) : Set E

Points carrying symmetric compatible scalar quotient-estimate data on the finite list of selected directions and their pairwise sums.

Equations

• AleksandrovDifferentiability.symmetricCompatibleDirectionalSliceQuotientEstimateSet D v u = {x : E | AleksandrovDifferentiability.SymmetricCompatibleDirectionalSliceQuotientEstimateAt D v u x}

def AleksandrovDifferentiability.directionalLineScalarEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : E) (u : E → ℝ) : Set E

Points where the line restriction in one fixed direction has scalar quadratic estimate data at the base parameter. This is the single-direction output expected from the later Fubini step.

Equations

• AleksandrovDifferentiability.directionalLineScalarEstimateSet v u = {x : E | AleksandrovDifferentiability.RealScalarQuadraticEstimateAt (AleksandrovDifferentiability.lineRestriction u x v) 0}

def AleksandrovDifferentiability.directionalLineScalarQuotientEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : E) (u : E → ℝ) : Set E

Points where the line restriction in one fixed direction has punctured normalized scalar quotient-estimate data at the base parameter.

Equations

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

@[simp]

theorem AleksandrovDifferentiability.mem_mixedDirectionalQuadraticEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} {x : E} : x ∈ mixedDirectionalQuadraticEstimateSet D v u ↔ MixedDirectionalQuadraticEstimateAt D v u x

@[simp]

theorem AleksandrovDifferentiability.mem_mixedDirectionalQuadraticQuotientEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} {x : E} : x ∈ mixedDirectionalQuadraticQuotientEstimateSet D v u ↔ MixedDirectionalQuadraticQuotientEstimateAt D v u x

@[simp]

theorem AleksandrovDifferentiability.mem_polarizedMixedDirectionalQuadraticEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {D : Finset ι} {v : ι → E} {u : E → ℝ} {x : E} : x ∈ polarizedMixedDirectionalQuadraticEstimateSet D v u ↔ PolarizedMixedDirectionalQuadraticEstimateAt D v u x

@[simp]

theorem AleksandrovDifferentiability.mem_polarizedMixedDirectionalQuadraticQuotientEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {D : Finset ι} {v : ι → E} {u : E → ℝ} {x : E} : x ∈ polarizedMixedDirectionalQuadraticQuotientEstimateSet D v u ↔ PolarizedMixedDirectionalQuadraticQuotientEstimateAt D v u x

@[simp]

theorem AleksandrovDifferentiability.mem_directionalSliceEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} {x : E} : x ∈ directionalSliceEstimateSet D v u ↔ DirectionalSliceEstimateAt D v u x

@[simp]

theorem AleksandrovDifferentiability.mem_compatibleDirectionalSliceEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} {x : E} : x ∈ compatibleDirectionalSliceEstimateSet D v u ↔ CompatibleDirectionalSliceEstimateAt D v u x

@[simp]

theorem AleksandrovDifferentiability.mem_symmetricCompatibleDirectionalSliceEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} {x : E} : x ∈ symmetricCompatibleDirectionalSliceEstimateSet D v u ↔ SymmetricCompatibleDirectionalSliceEstimateAt D v u x

@[simp]

theorem AleksandrovDifferentiability.mem_directionalSliceQuotientEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} {x : E} : x ∈ directionalSliceQuotientEstimateSet D v u ↔ DirectionalSliceQuotientEstimateAt D v u x

@[simp]

theorem AleksandrovDifferentiability.mem_compatibleDirectionalSliceQuotientEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} {x : E} : x ∈ compatibleDirectionalSliceQuotientEstimateSet D v u ↔ CompatibleDirectionalSliceQuotientEstimateAt D v u x

@[simp]

theorem AleksandrovDifferentiability.mem_symmetricCompatibleDirectionalSliceQuotientEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} {x : E} : x ∈ symmetricCompatibleDirectionalSliceQuotientEstimateSet D v u ↔ SymmetricCompatibleDirectionalSliceQuotientEstimateAt D v u x

@[simp]

theorem AleksandrovDifferentiability.mem_directionalLineScalarEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : E} {u : E → ℝ} {x : E} : x ∈ directionalLineScalarEstimateSet v u ↔ RealScalarQuadraticEstimateAt (lineRestriction u x v) 0

@[simp]

theorem AleksandrovDifferentiability.mem_directionalLineScalarQuotientEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : E} {u : E → ℝ} {x : E} : x ∈ directionalLineScalarQuotientEstimateSet v u ↔ RealScalarQuadraticQuotientEstimateAt (lineRestriction u x v) 0