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

Full-measure directional estimate assembly

This file turns directional scalar estimate sets and mixed-directional quadratic reconstruction data into full-measure second-order differentiability statements.

theorem AleksandrovDifferentiability.measure_diff_directionalLineScalarEstimateSet_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} (s : Set E) (u : E → ℝ) : μ (s \ directionalLineScalarEstimateSet 0 u) = 0

The zero-direction scalar estimate set has null complement inside every domain.

theorem AleksandrovDifferentiability.measure_diff_directionalLineScalarQuotientEstimateSet_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} (s : Set E) (u : E → ℝ) : μ (s \ directionalLineScalarQuotientEstimateSet 0 u) = 0

Quotient-estimate version of measure_diff_directionalLineScalarEstimateSet_zero.

theorem AleksandrovDifferentiability.ae_restrict_mem_directionalLineScalarEstimateSet_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} (s : Set E) (u : E → ℝ) : ∀ᵐ (x : E) ∂μ.restrict s, x ∈ directionalLineScalarEstimateSet 0 u

Almost-everywhere zero-direction scalar estimate membership inside every domain.

theorem AleksandrovDifferentiability.ae_restrict_mem_directionalLineScalarQuotientEstimateSet_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} (s : Set E) (u : E → ℝ) : ∀ᵐ (x : E) ∂μ.restrict s, x ∈ directionalLineScalarQuotientEstimateSet 0 u

Quotient-estimate version of ae_restrict_mem_directionalLineScalarEstimateSet_zero.

theorem AleksandrovDifferentiability.measure_diff_directionalLineScalarEstimateSet_smul_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} (s : Set E) {v : E} {c : ℝ} (hc : c ≠ 0) (u : E → ℝ) : μ (s \ directionalLineScalarEstimateSet (c • v) u) = μ (s \ directionalLineScalarEstimateSet v u)

Nonzero scalar rescaling of the direction preserves the null complement of the scalar directional-line good set.

theorem AleksandrovDifferentiability.measure_diff_directionalLineScalarQuotientEstimateSet_smul_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} (s : Set E) {v : E} {c : ℝ} (hc : c ≠ 0) (u : E → ℝ) : μ (s \ directionalLineScalarQuotientEstimateSet (c • v) u) = μ (s \ directionalLineScalarQuotientEstimateSet v u)

Quotient-estimate version of measure_diff_directionalLineScalarEstimateSet_smul_eq.

theorem AleksandrovDifferentiability.ae_restrict_mem_directionalLineScalarEstimateSet_smul_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} (s : Set E) {v : E} {c : ℝ} (hc : c ≠ 0) (u : E → ℝ) : (∀ᵐ (x : E) ∂μ.restrict s, x ∈ directionalLineScalarEstimateSet (c • v) u) ↔ ∀ᵐ (x : E) ∂μ.restrict s, x ∈ directionalLineScalarEstimateSet v u

Almost-everywhere scalar directional-line membership is invariant under nonzero scalar rescaling of the direction.

theorem AleksandrovDifferentiability.ae_restrict_mem_directionalLineScalarQuotientEstimateSet_smul_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} (s : Set E) {v : E} {c : ℝ} (hc : c ≠ 0) (u : E → ℝ) : (∀ᵐ (x : E) ∂μ.restrict s, x ∈ directionalLineScalarQuotientEstimateSet (c • v) u) ↔ ∀ᵐ (x : E) ∂μ.restrict s, x ∈ directionalLineScalarQuotientEstimateSet v u

Quotient-estimate version of ae_restrict_mem_directionalLineScalarEstimateSet_smul_iff.

theorem AleksandrovDifferentiability.measure_diff_directionalLineScalarQuotientEstimateSet_eq_zero_of_estimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {v : E} {u : E → ℝ} (hnull : μ (s \ directionalLineScalarEstimateSet v u) = 0) : μ (s \ directionalLineScalarQuotientEstimateSet v u) = 0

Full measure of the fixed-direction scalar estimate good set implies full measure of the corresponding punctured normalized quotient good set.

theorem AleksandrovDifferentiability.measure_diff_mixedDirectionalQuadraticQuotientSet_eq_zero_of_estimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {ι : Type u_2} {μ : MeasureTheory.Measure E} {s : Set E} {D : Finset ι} {v : ι → E} {u : E → ℝ} (hnull : μ (s \ mixedDirectionalQuadraticEstimateSet D v u) = 0) : μ (s \ mixedDirectionalQuadraticQuotientEstimateSet D v u) = 0

Full measure of the local mixed-directional quadratic estimate set implies full measure of its punctured normalized quotient-estimate version.

theorem AleksandrovDifferentiability.measure_diff_polarizedMixedDirectionalQuotientSet_eq_zero_of_estimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {ι : Type u_2} [DecidableEq ι] {μ : MeasureTheory.Measure E} {s : Set E} {D : Finset ι} {v : ι → E} {u : E → ℝ} (hnull : μ (s \ polarizedMixedDirectionalQuadraticEstimateSet D v u) = 0) : μ (s \ polarizedMixedDirectionalQuadraticQuotientEstimateSet D v u) = 0

Full measure of the local polarized mixed-directional quadratic estimate set implies full measure of its punctured normalized quotient-estimate version.

theorem AleksandrovDifferentiability.ae_restrict_mem_directionalLineScalarQuotientEstimateSet_of_estimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {v : E} {u : E → ℝ} (h : ∀ᵐ (x : E) ∂μ.restrict s, x ∈ directionalLineScalarEstimateSet v u) : ∀ᵐ (x : E) ∂μ.restrict s, x ∈ directionalLineScalarQuotientEstimateSet v u

Almost-everywhere membership in the fixed-direction scalar estimate good set implies almost-everywhere membership in the corresponding quotient good set.

theorem AleksandrovDifferentiability.ae_restrict_mem_mixedDirectionalQuadraticQuotientSet_of_estimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {ι : Type u_2} {μ : MeasureTheory.Measure E} {s : Set E} {D : Finset ι} {v : ι → E} {u : E → ℝ} (h : ∀ᵐ (x : E) ∂μ.restrict s, x ∈ mixedDirectionalQuadraticEstimateSet D v u) : ∀ᵐ (x : E) ∂μ.restrict s, x ∈ mixedDirectionalQuadraticQuotientEstimateSet D v u

Almost-everywhere membership in the mixed-directional estimate good set implies almost-everywhere membership in the corresponding quotient good set.

theorem AleksandrovDifferentiability.ae_restrict_mem_polarizedMixedDirectionalQuotientSet_of_estimateSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {ι : Type u_2} [DecidableEq ι] {μ : MeasureTheory.Measure E} {s : Set E} {D : Finset ι} {v : ι → E} {u : E → ℝ} (h : ∀ᵐ (x : E) ∂μ.restrict s, x ∈ polarizedMixedDirectionalQuadraticEstimateSet D v u) : ∀ᵐ (x : E) ∂μ.restrict s, x ∈ polarizedMixedDirectionalQuadraticQuotientEstimateSet D v u

Almost-everywhere membership in the polarized mixed-directional estimate good set implies almost-everywhere membership in the corresponding quotient good set.

theorem AleksandrovDifferentiability.ae_mem_directionalSliceEstimateSet_of_directionalLine_fullMeasure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {ι : Type u_2} {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (hs : MeasurableSet s) (D : Finset ι) (v : ι → E) (hpure : ∀ ⦃i : ι⦄, i ∈ D → μ (s \ directionalLineScalarEstimateSet (v i) u) = 0) (hpair : ∀ ⦃i : ι⦄, i ∈ D → ∀ ⦃j : ι⦄, j ∈ D → μ (s \ directionalLineScalarEstimateSet (v i + v j) u) = 0) : ∀ᵐ (x : E) ∂μ.restrict s, x ∈ directionalSliceEstimateSet D v u

Finite bookkeeping for directional slices: if each selected pure direction and each selected pairwise-sum direction has scalar estimate data on a full-measure subset of s, then the bundled finite directional slice target holds a.e. on s.

theorem AleksandrovDifferentiability.measure_diff_directionalSliceEstimateSet_eq_zero_of_directionalLine_fullMeasure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {ι : Type u_2} {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (hs : MeasurableSet s) (D : Finset ι) (v : ι → E) (hpure : ∀ ⦃i : ι⦄, i ∈ D → μ (s \ directionalLineScalarEstimateSet (v i) u) = 0) (hpair : ∀ ⦃i : ι⦄, i ∈ D → ∀ ⦃j : ι⦄, j ∈ D → μ (s \ directionalLineScalarEstimateSet (v i + v j) u) = 0) : μ (s \ directionalSliceEstimateSet D v u) = 0

Null-complement form of ae_mem_directionalSliceEstimateSet_of_directionalLine_fullMeasure.

theorem AleksandrovDifferentiability.ae_mem_directionalSliceEstimateSet_of_directionalLine_fullMeasure_offDiagonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {ι : Type u_2} {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (hs : MeasurableSet s) (D : Finset ι) (v : ι → E) (hpure : ∀ ⦃i : ι⦄, i ∈ D → μ (s \ directionalLineScalarEstimateSet (v i) u) = 0) (hpair : ∀ ⦃i : ι⦄, i ∈ D → ∀ ⦃j : ι⦄, j ∈ D → i ≠ j → μ (s \ directionalLineScalarEstimateSet (v i + v j) u) = 0) : ∀ᵐ (x : E) ∂μ.restrict s, x ∈ directionalSliceEstimateSet D v u

Off-diagonal version of ae_mem_directionalSliceEstimateSet_of_directionalLine_fullMeasure: pairwise full-measure hypotheses are only needed when the two selected directions are different.

theorem AleksandrovDifferentiability.measure_diff_directionalSliceSet_eq_zero_of_directionalLine_fullMeasure_offDiagonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {ι : Type u_2} {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (hs : MeasurableSet s) (D : Finset ι) (v : ι → E) (hpure : ∀ ⦃i : ι⦄, i ∈ D → μ (s \ directionalLineScalarEstimateSet (v i) u) = 0) (hpair : ∀ ⦃i : ι⦄, i ∈ D → ∀ ⦃j : ι⦄, j ∈ D → i ≠ j → μ (s \ directionalLineScalarEstimateSet (v i + v j) u) = 0) : μ (s \ directionalSliceEstimateSet D v u) = 0

Null-complement form of ae_mem_directionalSliceEstimateSet_of_directionalLine_fullMeasure_offDiagonal.

theorem AleksandrovDifferentiability.ae_mem_directionalSliceQuotientSet_of_directionalLine_fullMeasure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {ι : Type u_2} {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (hs : MeasurableSet s) (D : Finset ι) (v : ι → E) (hpure : ∀ ⦃i : ι⦄, i ∈ D → μ (s \ directionalLineScalarQuotientEstimateSet (v i) u) = 0) (hpair : ∀ ⦃i : ι⦄, i ∈ D → ∀ ⦃j : ι⦄, j ∈ D → μ (s \ directionalLineScalarQuotientEstimateSet (v i + v j) u) = 0) : ∀ᵐ (x : E) ∂μ.restrict s, x ∈ directionalSliceQuotientEstimateSet D v u

Quotient-estimate version of ae_mem_directionalSliceEstimateSet_of_directionalLine_fullMeasure.

theorem AleksandrovDifferentiability.measure_diff_directionalSliceQuotientSet_eq_zero_of_directionalLine_fullMeasure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {ι : Type u_2} {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (hs : MeasurableSet s) (D : Finset ι) (v : ι → E) (hpure : ∀ ⦃i : ι⦄, i ∈ D → μ (s \ directionalLineScalarQuotientEstimateSet (v i) u) = 0) (hpair : ∀ ⦃i : ι⦄, i ∈ D → ∀ ⦃j : ι⦄, j ∈ D → μ (s \ directionalLineScalarQuotientEstimateSet (v i + v j) u) = 0) : μ (s \ directionalSliceQuotientEstimateSet D v u) = 0

Null-complement form of ae_mem_directionalSliceQuotientSet_of_directionalLine_fullMeasure.

theorem AleksandrovDifferentiability.measure_diff_directionalSliceQuotientSet_eq_zero_of_directionalLineEstimate_fullMeasure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {ι : Type u_2} {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (hs : MeasurableSet s) (D : Finset ι) (v : ι → E) (hpure : ∀ ⦃i : ι⦄, i ∈ D → μ (s \ directionalLineScalarEstimateSet (v i) u) = 0) (hpair : ∀ ⦃i : ι⦄, i ∈ D → ∀ ⦃j : ι⦄, j ∈ D → μ (s \ directionalLineScalarEstimateSet (v i + v j) u) = 0) : μ (s \ directionalSliceQuotientEstimateSet D v u) = 0

Non-quotient scalar line full-measure hypotheses imply full measure of the finite quotient slice target.

theorem AleksandrovDifferentiability.ae_mem_directionalSliceQuotientSet_of_directionalLine_fullMeasure_offDiagonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {ι : Type u_2} {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (hs : MeasurableSet s) (D : Finset ι) (v : ι → E) (hpure : ∀ ⦃i : ι⦄, i ∈ D → μ (s \ directionalLineScalarQuotientEstimateSet (v i) u) = 0) (hpair : ∀ ⦃i : ι⦄, i ∈ D → ∀ ⦃j : ι⦄, j ∈ D → i ≠ j → μ (s \ directionalLineScalarQuotientEstimateSet (v i + v j) u) = 0) : ∀ᵐ (x : E) ∂μ.restrict s, x ∈ directionalSliceQuotientEstimateSet D v u

Off-diagonal quotient-estimate version of ae_mem_directionalSliceEstimateSet_of_directionalLine_fullMeasure_offDiagonal.

theorem AleksandrovDifferentiability.measure_diff_directionalSliceQuotientSet_eq_zero_of_directionalLine_fullMeasure_offDiagonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {ι : Type u_2} {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (hs : MeasurableSet s) (D : Finset ι) (v : ι → E) (hpure : ∀ ⦃i : ι⦄, i ∈ D → μ (s \ directionalLineScalarQuotientEstimateSet (v i) u) = 0) (hpair : ∀ ⦃i : ι⦄, i ∈ D → ∀ ⦃j : ι⦄, j ∈ D → i ≠ j → μ (s \ directionalLineScalarQuotientEstimateSet (v i + v j) u) = 0) : μ (s \ directionalSliceQuotientEstimateSet D v u) = 0

Null-complement form of ae_mem_directionalSliceQuotientSet_of_directionalLine_fullMeasure_offDiagonal.

theorem AleksandrovDifferentiability.measure_diff_directionalSliceQuotientSet_eq_zero_of_directionalLineEstimate_fullMeasure_offDiag {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {ι : Type u_2} {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (hs : MeasurableSet s) (D : Finset ι) (v : ι → E) (hpure : ∀ ⦃i : ι⦄, i ∈ D → μ (s \ directionalLineScalarEstimateSet (v i) u) = 0) (hpair : ∀ ⦃i : ι⦄, i ∈ D → ∀ ⦃j : ι⦄, j ∈ D → i ≠ j → μ (s \ directionalLineScalarEstimateSet (v i + v j) u) = 0) : μ (s \ directionalSliceQuotientEstimateSet D v u) = 0

Off-diagonal version of measure_diff_directionalSliceQuotientSet_eq_zero_of_directionalLineEstimate_fullMeasure.

theorem AleksandrovDifferentiability.measure_diff_compatibleDirectionalSliceQuotientSet_eq_zero_of_compatibleSliceSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {ι : Type u_2} {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (D : Finset ι) (v : ι → E) (hnull : μ (s \ compatibleDirectionalSliceEstimateSet D v u) = 0) : μ (s \ compatibleDirectionalSliceQuotientEstimateSet D v u) = 0

Full measure of the compatible finite slice target implies full measure of the compatible finite quotient-slice target.

theorem AleksandrovDifferentiability.measure_diff_directionalSliceQuotientSet_eq_zero_of_compatibleSliceSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {ι : Type u_2} {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (D : Finset ι) (v : ι → E) (hnull : μ (s \ compatibleDirectionalSliceEstimateSet D v u) = 0) : μ (s \ directionalSliceQuotientEstimateSet D v u) = 0

Full measure of the compatible finite slice target also implies full measure of the older existential finite quotient-slice target.

theorem AleksandrovDifferentiability.measure_diff_symmetricCompatibleSliceSet_eq_zero_of_compatibleSliceSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {ι : Type u_2} {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (D : Finset ι) (v : ι → E) (hnull : μ (s \ compatibleDirectionalSliceEstimateSet D v u) = 0) : μ (s \ symmetricCompatibleDirectionalSliceEstimateSet D v u) = 0

Full measure of the compatible finite slice target implies full measure of the symmetric compatible finite slice target.

theorem AleksandrovDifferentiability.measure_diff_symmetricCompatibleSliceQuotientSet_eq_zero_of_compatibleSliceQuotientSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {ι : Type u_2} {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (D : Finset ι) (v : ι → E) (hnull : μ (s \ compatibleDirectionalSliceQuotientEstimateSet D v u) = 0) : μ (s \ symmetricCompatibleDirectionalSliceQuotientEstimateSet D v u) = 0

Full measure of the compatible finite quotient-slice target implies full measure of the symmetric compatible finite quotient-slice target.

theorem AleksandrovDifferentiability.measure_diff_symmetricCompatibleSliceQuotientSet_eq_zero_of_compatibleSliceSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {ι : Type u_2} {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (D : Finset ι) (v : ι → E) (hnull : μ (s \ compatibleDirectionalSliceEstimateSet D v u) = 0) : μ (s \ symmetricCompatibleDirectionalSliceQuotientEstimateSet D v u) = 0

Full measure of the compatible finite slice target implies full measure of the symmetric compatible finite quotient-slice target.

theorem AleksandrovDifferentiability.measure_diff_symmetricCompatibleSliceQuotientSet_eq_zero_of_symmetricSliceSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {ι : Type u_2} {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (D : Finset ι) (v : ι → E) (hnull : μ (s \ symmetricCompatibleDirectionalSliceEstimateSet D v u) = 0) : μ (s \ symmetricCompatibleDirectionalSliceQuotientEstimateSet D v u) = 0

Full measure of the symmetric compatible finite slice target implies full measure of the symmetric compatible finite quotient-slice target.