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

Reconstruction from directional quadratic data

This file converts mixed directional quadratic estimate data into the project-local second-order differentiability predicate.

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

Mixed-directional quadratic estimate data implies second-order differentiability.

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

Mixed-directional quadratic quotient data implies second-order differentiability.

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

Polarized coefficient estimate data is a special case of mixed-directional estimate data.

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

Punctured normalized polarized coefficient estimate data is a special case of mixed-directional quotient estimate data.

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

Polarized mixed-directional estimate data implies second-order differentiability.

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

Polarized mixed-directional quotient estimate data implies second-order differentiability.

theorem AleksandrovDifferentiability.polarizedMixedDirectionalQuadraticEstimateAt_of_quadraticEstimateData_coefficients {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {D : Finset ι} {v : ι → E} (hv : FiniteOrthonormalSpanningOn D v) {u : E → ℝ} {x p : E} {B : E →L[ℝ] E} (hB : IsSymmetricOperator B) {q : ι → ℝ} {r : ι → ι → ℝ} (hest : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (z : E) in nhds 0, ‖affineRemainder u x p (x + z) - 1 / 2 * inner ℝ z (B z)‖ ≤ ε * ‖z‖ ^ 2) (hr : ∀ ⦃i : ι⦄, i ∈ D → ∀ ⦃j : ι⦄, j ∈ D → r j i = r i j) (hpure : ∀ ⦃i : ι⦄, i ∈ D → inner ℝ (v i) (B (v i)) = q i) (hpair : ∀ ⦃i : ι⦄, i ∈ D → ∀ ⦃j : ι⦄, j ∈ D → i ≠ j → inner ℝ (v i + v j) (B (v i + v j)) = r i j) : PolarizedMixedDirectionalQuadraticEstimateAt D v u x

If a symmetric ambient quadratic estimate has the prescribed pure and off-diagonal pairwise-sum quadratic coefficients on a finite orthonormal spanning frame, then it is the canonical polarized mixed-directional estimate. The algebraic identification of the Hessian candidate is handled by finite-frame off-diagonal uniqueness.

theorem AleksandrovDifferentiability.polarizedMixedDirectionalQuadraticQuotientEstimateAt_of_quadraticQuotientData_coefficients {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {D : Finset ι} {v : ι → E} (hv : FiniteOrthonormalSpanningOn D v) {u : E → ℝ} {x p : E} {B : E →L[ℝ] E} (hB : IsSymmetricOperator B) {q : ι → ℝ} {r : ι → ι → ℝ} (hest : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (z : E) in nhdsWithin 0 {z : E | z ≠ 0}, ‖affineRemainder u x p (x + z) - 1 / 2 * inner ℝ z (B z)‖ / ‖z‖ ^ 2 ≤ ε) (hr : ∀ ⦃i : ι⦄, i ∈ D → ∀ ⦃j : ι⦄, j ∈ D → r j i = r i j) (hpure : ∀ ⦃i : ι⦄, i ∈ D → inner ℝ (v i) (B (v i)) = q i) (hpair : ∀ ⦃i : ι⦄, i ∈ D → ∀ ⦃j : ι⦄, j ∈ D → i ≠ j → inner ℝ (v i + v j) (B (v i + v j)) = r i j) : PolarizedMixedDirectionalQuadraticQuotientEstimateAt D v u x

Punctured normalized quotient version of polarizedMixedDirectionalQuadraticEstimateAt_of_quadraticEstimateData_coefficients.

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

A local mixed-directional estimate gives the punctured normalized quotient estimate with the same directional coefficient matrix.

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

A local polarized mixed-directional estimate gives the punctured normalized quotient estimate with the same pure and pairwise-sum coefficients.

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

Mixed-directional quadratic estimate data is ambient quadratic estimate data with the assembled mixed-directional Hessian candidate.

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

Mixed-directional quotient estimate data is ambient quadratic quotient estimate data with the assembled mixed-directional Hessian candidate.

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

Polarized mixed-directional quadratic estimate data is ambient quadratic estimate data.

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

Polarized mixed-directional quotient estimate data is ambient quadratic quotient estimate data.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticEstimateSet_subset_secondOrderDifferentiabilitySet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} : mixedDirectionalQuadraticEstimateSet D v u ⊆ secondOrderDifferentiabilitySet u

The mixed-directional estimate set is contained in the second-order differentiability locus.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticQuotientEstimateSet_subset_secondOrderDifferentiabilitySet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} : mixedDirectionalQuadraticQuotientEstimateSet D v u ⊆ secondOrderDifferentiabilitySet u

The mixed-directional quotient-estimate set is contained in the second-order differentiability locus.

theorem AleksandrovDifferentiability.polarizedMixedDirectionalQuadraticEstimateSet_subset_mixedDirectionalQuadraticEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {D : Finset ι} {v : ι → E} {u : E → ℝ} : polarizedMixedDirectionalQuadraticEstimateSet D v u ⊆ mixedDirectionalQuadraticEstimateSet D v u

The polarized mixed-directional estimate set is contained in the mixed-directional estimate set.

theorem AleksandrovDifferentiability.polarizedMixedDirectionalQuotientSet_subset_mixedDirectionalQuotientSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {D : Finset ι} {v : ι → E} {u : E → ℝ} : polarizedMixedDirectionalQuadraticQuotientEstimateSet D v u ⊆ mixedDirectionalQuadraticQuotientEstimateSet D v u

The polarized mixed-directional quotient estimate set is contained in the mixed-directional quotient estimate set.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticEstimateSet_subset_mixedDirectionalQuadraticQuotientSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} : mixedDirectionalQuadraticEstimateSet D v u ⊆ mixedDirectionalQuadraticQuotientEstimateSet D v u

The local mixed-directional estimate set is contained in its punctured normalized quotient version.

theorem AleksandrovDifferentiability.polarizedMixedDirectionalQuadraticSet_subset_polarizedMixedDirectionalQuadraticQuotientSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {D : Finset ι} {v : ι → E} {u : E → ℝ} : polarizedMixedDirectionalQuadraticEstimateSet D v u ⊆ polarizedMixedDirectionalQuadraticQuotientEstimateSet D v u

The local polarized mixed-directional estimate set is contained in its punctured normalized quotient version.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticEstimateSet_subset_quadraticEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} : mixedDirectionalQuadraticEstimateSet D v u ⊆ quadraticEstimateSet u

The mixed-directional estimate set is contained in the generic ambient quadratic estimate set.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticQuotientSet_subset_quadraticQuotientEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} : mixedDirectionalQuadraticQuotientEstimateSet D v u ⊆ quadraticQuotientEstimateSet u

The mixed-directional quotient-estimate set is contained in the generic ambient quadratic quotient-estimate set.

theorem AleksandrovDifferentiability.polarizedMixedDirectionalQuadraticSet_subset_quadraticEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {D : Finset ι} {v : ι → E} {u : E → ℝ} : polarizedMixedDirectionalQuadraticEstimateSet D v u ⊆ quadraticEstimateSet u

The polarized mixed-directional estimate set is contained in the generic ambient quadratic estimate set.

theorem AleksandrovDifferentiability.polarizedMixedDirectionalQuotientSet_subset_quadraticQuotientEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {D : Finset ι} {v : ι → E} {u : E → ℝ} : polarizedMixedDirectionalQuadraticQuotientEstimateSet D v u ⊆ quadraticQuotientEstimateSet u

The polarized mixed-directional quotient-estimate set is contained in the generic ambient quadratic quotient-estimate set.

theorem AleksandrovDifferentiability.polarizedMixedDirectionalQuadraticEstimateSet_subset_secondOrderDifferentiabilitySet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {D : Finset ι} {v : ι → E} {u : E → ℝ} : polarizedMixedDirectionalQuadraticEstimateSet D v u ⊆ secondOrderDifferentiabilitySet u

The polarized mixed-directional estimate set is contained in the second-order differentiability locus.

theorem AleksandrovDifferentiability.polarizedMixedDirectionalQuadraticQuotientEstimateSet_subset_secondOrderDifferentiabilitySet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {D : Finset ι} {v : ι → E} {u : E → ℝ} : polarizedMixedDirectionalQuadraticQuotientEstimateSet D v u ⊆ secondOrderDifferentiabilitySet u

The polarized mixed-directional quotient estimate set is contained in the second-order differentiability locus.

theorem AleksandrovDifferentiability.MixedDirectionalQuadraticEstimateAt.realScalarQuadraticEstimateAt_lineRestriction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} {x : E} (h : MixedDirectionalQuadraticEstimateAt D v u x) (w : E) : RealScalarQuadraticEstimateAt (lineRestriction u x w) 0

Mixed-directional quadratic estimate data restricts to scalar quadratic estimate data on every affine line through the base point.

theorem AleksandrovDifferentiability.MixedDirectionalQuadraticEstimateAt.realScalarQuadraticEstimateWithDataAt_lineRestriction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} {x : E} (h : MixedDirectionalQuadraticEstimateAt D v u x) (w : E) : ∃ (p : E) (a : ι → ι → ℝ), RealScalarQuadraticEstimateWithDataAt (lineRestriction u x w) 0 (inner ℝ p w) (inner ℝ w ((mixedDirectionalQuadraticSum D v a) w))

Mixed-directional quadratic estimate data restricts to scalar quadratic estimate data with the line slope and quadratic coefficient specified by the ambient data.

theorem AleksandrovDifferentiability.MixedDirectionalQuadraticQuotientEstimateAt.realScalarQuadraticEstimateAt_lineRestriction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} {x : E} (h : MixedDirectionalQuadraticQuotientEstimateAt D v u x) (w : E) : RealScalarQuadraticEstimateAt (lineRestriction u x w) 0

Mixed-directional punctured quotient estimate data restricts to scalar quadratic estimate data on every affine line through the base point.

theorem AleksandrovDifferentiability.MixedDirectionalQuadraticQuotientEstimateAt.scalarQuotientWithData_lineRestriction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} {x : E} (h : MixedDirectionalQuadraticQuotientEstimateAt D v u x) (w : E) : ∃ (p : E) (a : ι → ι → ℝ), RealScalarQuadraticQuotientEstimateWithDataAt (lineRestriction u x w) 0 (inner ℝ p w) (inner ℝ w ((mixedDirectionalQuadraticSum D v a) w))

Mixed-directional punctured quotient estimate data restricts to explicit scalar quotient estimate data with the line slope and quadratic coefficient specified by the ambient data.

theorem AleksandrovDifferentiability.MixedDirectionalQuadraticEstimateAt.realScalarQuadraticQuotientEstimateAt_lineRestriction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} {x : E} (h : MixedDirectionalQuadraticEstimateAt D v u x) (w : E) : RealScalarQuadraticQuotientEstimateAt (lineRestriction u x w) 0

Mixed-directional quadratic estimate data restricts to punctured scalar quotient-estimate data on every affine line through the base point.

theorem AleksandrovDifferentiability.MixedDirectionalQuadraticQuotientEstimateAt.scalarQuotientEstimateAt_lineRestriction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} {x : E} (h : MixedDirectionalQuadraticQuotientEstimateAt D v u x) (w : E) : RealScalarQuadraticQuotientEstimateAt (lineRestriction u x w) 0

Mixed-directional punctured quotient estimate data restricts to punctured scalar quotient-estimate data on every affine line through the base point.

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

Mixed-directional quadratic estimate data implies the finite slice-estimate target for the selected directions and their pairwise sums.

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

Mixed-directional quadratic estimate data implies compatible finite slice data: all one-dimensional first-order coefficients come from the same ambient slope.

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

Mixed-directional quadratic estimate data implies symmetric-compatible finite slice data. The pairwise coefficients are read directly from the ambient quadratic model, so reversing the order of the two selected directions does not change them.

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

Mixed-directional quadratic estimate data implies the finite slice quotient-estimate target for the selected directions and their pairwise sums.

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

Mixed-directional quotient estimate data implies the finite slice-estimate target for the selected directions and their pairwise sums.

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

Mixed-directional quotient estimate data implies compatible finite quotient-slice data.

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

Mixed-directional quotient estimate data implies symmetric-compatible finite quotient-slice data.

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

Mixed-directional quotient estimate data implies the finite slice quotient-estimate target for the selected directions and their pairwise sums.

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

Polarized mixed-directional quadratic estimate data implies the finite slice-estimate target for the selected directions and their pairwise sums.

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

Polarized mixed-directional quadratic estimate data implies compatible finite slice data.

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

Polarized mixed-directional quadratic estimate data implies symmetric-compatible finite slice data.

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

Polarized mixed-directional quadratic estimate data implies the finite slice quotient target for the selected directions and their pairwise sums.

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

Polarized mixed-directional quotient estimate data implies the finite slice-estimate target for the selected directions and their pairwise sums.

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

Polarized mixed-directional quotient estimate data implies compatible finite quotient-slice data.

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

Polarized mixed-directional quotient estimate data implies symmetric-compatible finite quotient-slice data.

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

Polarized mixed-directional quotient estimate data implies the finite slice quotient target for the selected directions and their pairwise sums.

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

Compatible finite slice data forgets to the existential finite slice target.

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

Symmetric compatible finite slice data forgets to compatible finite slice data.

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

Compatible finite slice data can be represented with symmetric pairwise-sum coefficients by averaging the two ordered pair coefficients.

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

Compatible finite quotient-slice data forgets to the existential finite quotient-slice target.

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

Symmetric compatible finite quotient-slice data forgets to compatible finite quotient-slice data.

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

Compatible finite quotient-slice data can be represented with symmetric pairwise-sum coefficients by averaging the two ordered pair coefficients.

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

Compatible finite slice data gives compatible finite quotient-slice data with the same ambient slope and scalar quadratic coefficients.

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

Symmetric compatible finite slice data gives symmetric compatible finite quotient-slice data with the same ambient slope and scalar quadratic coefficients.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticEstimateSet_subset_lineScalarEstimateAtZero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} {w : E} : mixedDirectionalQuadraticEstimateSet D v u ⊆ {x : E | 0 ∈ realScalarQuadraticEstimateSet (lineRestriction u x w)}

Points with mixed-directional estimate data restrict to scalar estimate points on every affine line through the base point.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticQuotientEstimateSet_subset_lineScalarQuotientEstimateAtZero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} {w : E} : mixedDirectionalQuadraticQuotientEstimateSet D v u ⊆ {x : E | 0 ∈ realScalarQuadraticQuotientEstimateSet (lineRestriction u x w)}

Points with mixed-directional quotient estimate data restrict to scalar quotient-estimate points on every affine line through the base point.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticEstimateSet_subset_directionalSliceEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} : mixedDirectionalQuadraticEstimateSet D v u ⊆ directionalSliceEstimateSet D v u

The mixed-directional estimate set is contained in the finite directional slice-estimate set.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticEstimateSet_subset_compatibleDirectionalSliceEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} : mixedDirectionalQuadraticEstimateSet D v u ⊆ compatibleDirectionalSliceEstimateSet D v u

The mixed-directional estimate set is contained in the compatible finite slice-estimate set.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticEstimateSet_subset_symmetricCompatibleDirectionalSliceEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} : mixedDirectionalQuadraticEstimateSet D v u ⊆ symmetricCompatibleDirectionalSliceEstimateSet D v u

The mixed-directional estimate set is contained in the symmetric-compatible finite slice-estimate set.

theorem AleksandrovDifferentiability.compatibleDirectionalSliceEstimateSet_subset_symmetricCompatibleDirectionalSliceEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} : compatibleDirectionalSliceEstimateSet D v u ⊆ symmetricCompatibleDirectionalSliceEstimateSet D v u

The compatible finite slice-estimate set is contained in the symmetric compatible finite slice-estimate set.

theorem AleksandrovDifferentiability.directionalSliceEstimateAt_of_pure_offDiagonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} {x : E} (hpure : ∀ ⦃i : ι⦄, i ∈ D → RealScalarQuadraticEstimateAt (lineRestriction u x (v i)) 0) (hpair : ∀ ⦃i : ι⦄, i ∈ D → ∀ ⦃j : ι⦄, j ∈ D → i ≠ j → RealScalarQuadraticEstimateAt (lineRestriction u x (v i + v j)) 0) : DirectionalSliceEstimateAt D v u x

Pure directional scalar estimates plus off-diagonal pairwise-sum estimates give the bundled finite slice target. The diagonal pair directions are supplied by rescaling the pure estimates.

theorem AleksandrovDifferentiability.directionalSliceQuotientEstimateAt_of_pure_offDiagonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} {x : E} (hpure : ∀ ⦃i : ι⦄, i ∈ D → RealScalarQuadraticQuotientEstimateAt (lineRestriction u x (v i)) 0) (hpair : ∀ ⦃i : ι⦄, i ∈ D → ∀ ⦃j : ι⦄, j ∈ D → i ≠ j → RealScalarQuadraticQuotientEstimateAt (lineRestriction u x (v i + v j)) 0) : DirectionalSliceQuotientEstimateAt D v u x

Quotient-estimate version of directionalSliceEstimateAt_of_pure_offDiagonal.

theorem AleksandrovDifferentiability.symmetricCompatibleDirectionalSliceEstimateSet_subset_compatibleDirectionalSliceEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} : symmetricCompatibleDirectionalSliceEstimateSet D v u ⊆ compatibleDirectionalSliceEstimateSet D v u

The symmetric compatible finite slice-estimate set is contained in the compatible finite slice-estimate set.

theorem AleksandrovDifferentiability.compatibleDirectionalSliceEstimateSet_subset_directionalSliceEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} : compatibleDirectionalSliceEstimateSet D v u ⊆ directionalSliceEstimateSet D v u

The compatible finite slice-estimate set is contained in the older existential finite slice-estimate set.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticEstimateSet_subset_directionalSliceQuotientEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} : mixedDirectionalQuadraticEstimateSet D v u ⊆ directionalSliceQuotientEstimateSet D v u

The mixed-directional estimate set is contained in the finite directional slice quotient-estimate set.

theorem AleksandrovDifferentiability.compatibleDirectionalSliceEstimateSet_subset_compatibleDirectionalSliceQuotientEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} : compatibleDirectionalSliceEstimateSet D v u ⊆ compatibleDirectionalSliceQuotientEstimateSet D v u

The compatible finite slice-estimate set is contained in the compatible finite quotient-slice estimate set.

theorem AleksandrovDifferentiability.symmetricCompatibleDirectionalSliceEstimateSet_subset_symmetricCompatibleQuotientSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} : symmetricCompatibleDirectionalSliceEstimateSet D v u ⊆ symmetricCompatibleDirectionalSliceQuotientEstimateSet D v u

The symmetric compatible finite slice-estimate set is contained in the symmetric compatible finite quotient-slice estimate set.

theorem AleksandrovDifferentiability.compatibleDirectionalSliceQuotientEstimateSet_subset_directionalSliceQuotientEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} : compatibleDirectionalSliceQuotientEstimateSet D v u ⊆ directionalSliceQuotientEstimateSet D v u

The compatible finite quotient-slice estimate set is contained in the older existential finite quotient-slice estimate set.

theorem AleksandrovDifferentiability.compatibleDirectionalSliceEstimateSet_subset_directionalSliceQuotientEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} : compatibleDirectionalSliceEstimateSet D v u ⊆ directionalSliceQuotientEstimateSet D v u

The compatible finite slice-estimate set is contained in the older existential finite quotient-slice estimate set.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticQuotientEstimateSet_subset_directionalSliceEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} : mixedDirectionalQuadraticQuotientEstimateSet D v u ⊆ directionalSliceEstimateSet D v u

The mixed-directional quotient-estimate set is contained in the finite directional slice-estimate set.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticQuotientEstimateSet_subset_directionalSliceQuotientEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} : mixedDirectionalQuadraticQuotientEstimateSet D v u ⊆ directionalSliceQuotientEstimateSet D v u

The mixed-directional quotient-estimate set is contained in the finite directional slice quotient-estimate set.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticQuotientEstimateSet_subset_compatibleDirectionalSliceQuotientSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} : mixedDirectionalQuadraticQuotientEstimateSet D v u ⊆ compatibleDirectionalSliceQuotientEstimateSet D v u

The mixed-directional quotient-estimate set is contained in the compatible finite quotient-slice estimate set.

theorem AleksandrovDifferentiability.mixedDirectionalQuadraticQuotientEstimateSet_subset_symmetricCompatibleQuotientSliceSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} : mixedDirectionalQuadraticQuotientEstimateSet D v u ⊆ symmetricCompatibleDirectionalSliceQuotientEstimateSet D v u

The mixed-directional quotient-estimate set is contained in the symmetric-compatible finite quotient-slice estimate set.

theorem AleksandrovDifferentiability.compatibleDirectionalSliceQuotientSet_subset_symmetricCompatibleDirectionalSliceQuotientSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} : compatibleDirectionalSliceQuotientEstimateSet D v u ⊆ symmetricCompatibleDirectionalSliceQuotientEstimateSet D v u

The compatible finite quotient-slice estimate set is contained in the symmetric compatible finite quotient-slice estimate set.

theorem AleksandrovDifferentiability.symmetricCompatibleDirectionalSliceQuotientSet_subset_compatibleDirectionalSliceQuotientSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {D : Finset ι} {v : ι → E} {u : E → ℝ} : symmetricCompatibleDirectionalSliceQuotientEstimateSet D v u ⊆ compatibleDirectionalSliceQuotientEstimateSet D v u

The symmetric compatible finite quotient-slice estimate set is contained in the compatible finite quotient-slice estimate set.

theorem AleksandrovDifferentiability.polarizedMixedDirectionalQuadraticSet_subset_directionalSliceEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {D : Finset ι} {v : ι → E} {u : E → ℝ} : polarizedMixedDirectionalQuadraticEstimateSet D v u ⊆ directionalSliceEstimateSet D v u

The polarized mixed-directional estimate set is contained in the finite directional slice-estimate set.

theorem AleksandrovDifferentiability.polarizedMixedDirectionalQuadraticSet_subset_directionalSliceQuotientSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {D : Finset ι} {v : ι → E} {u : E → ℝ} : polarizedMixedDirectionalQuadraticEstimateSet D v u ⊆ directionalSliceQuotientEstimateSet D v u

The polarized mixed-directional estimate set is contained in the finite directional slice quotient-estimate set.

theorem AleksandrovDifferentiability.polarizedMixedDirectionalQuadraticSet_subset_compatibleDirectionalSliceEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {D : Finset ι} {v : ι → E} {u : E → ℝ} : polarizedMixedDirectionalQuadraticEstimateSet D v u ⊆ compatibleDirectionalSliceEstimateSet D v u

The polarized mixed-directional estimate set is contained in the compatible finite slice-estimate set.

theorem AleksandrovDifferentiability.polarizedMixedDirectionalQuotientSet_subset_directionalSliceEstimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {D : Finset ι} {v : ι → E} {u : E → ℝ} : polarizedMixedDirectionalQuadraticQuotientEstimateSet D v u ⊆ directionalSliceEstimateSet D v u

The polarized mixed-directional quotient estimate set is contained in the finite directional slice-estimate set.

theorem AleksandrovDifferentiability.polarizedMixedDirectionalQuotientSet_subset_directionalSliceQuotientSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {D : Finset ι} {v : ι → E} {u : E → ℝ} : polarizedMixedDirectionalQuadraticQuotientEstimateSet D v u ⊆ directionalSliceQuotientEstimateSet D v u

The polarized mixed-directional quotient estimate set is contained in the finite directional slice quotient-estimate set.

theorem AleksandrovDifferentiability.polarizedMixedDirectionalQuotientSet_subset_compatibleDirectionalSliceQuotientSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [DecidableEq ι] {D : Finset ι} {v : ι → E} {u : E → ℝ} : polarizedMixedDirectionalQuadraticQuotientEstimateSet D v u ⊆ compatibleDirectionalSliceQuotientEstimateSet D v u

The polarized mixed-directional quotient-estimate set is contained in the compatible finite quotient-slice estimate set.