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

Localization from source cubes to affine images

This file starts the final source-document localization step. The first lemma separates the pointwise chain-rule part from the still-remaining measure-identification and countable-cover arguments: a.e. second-order differentiability of the pullback z ↦ u (a + r • z) pushes forward to a.e. second-order differentiability of u with respect to the image measure.

def AleksandrovDifferentiability.sourceAffineCubeImage (n : ℕ) (a : SourceCubeSpace n) (r R : ℝ) : Set (SourceCubeSpace n)

The affine image a + r • Q_R of a source cube.

Equations

• AleksandrovDifferentiability.sourceAffineCubeImage n a r R = (fun (z : AleksandrovDifferentiability.SourceCubeSpace n) => a + r • z) '' AleksandrovDifferentiability.sourceOpenCube n R

theorem AleksandrovDifferentiability.sourceAffineCubeImage_subset_of_le {n : ℕ} (a : SourceCubeSpace n) (r : ℝ) {R S : ℝ} (hRS : R ≤ S) : sourceAffineCubeImage n a r R ⊆ sourceAffineCubeImage n a r S

Affine source-cube images are monotone in the source radius.

def AleksandrovDifferentiability.SourceAffineCubeCoverIndex (n : ℕ) (Ω : Set (SourceCubeSpace n)) : Type

Parameters for affine source cubes whose enlarged Q_3 image stays inside Ω.

Equations

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

def AleksandrovDifferentiability.SourceAffineCompactCubeCoverIndex (n : ℕ) (Ω : Set (SourceCubeSpace n)) : Type

Parameters for affine source cubes with enough extra room to bound the Q_3 pullback.

The normalized theorem assumes boundedness on Q_3. For an arbitrary finite convex function on an open set, this boundedness is obtained from continuity on a compact cube sitting strictly inside the domain. Recording that the larger open image a + r • Q_4 lies in Ω gives that compact room for the closed Q_3 cube.

Equations

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

theorem AleksandrovDifferentiability.ae_restrict_of_subset_iUnion_of_ae_restrict {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Countable ι] {μ : MeasureTheory.Measure α} {Ω : Set α} {U : ι → Set α} {p : α → Prop} (hcover : Ω ⊆ ⋃ (i : ι), U i) (hU : ∀ (i : ι), ∀ᵐ (x : α) ∂μ.restrict (U i), p x) : ∀ᵐ (x : α) ∂μ.restrict Ω, p x

Assemble restricted a.e. statements across a countable cover.

This is the measure-theoretic core of the source localization step: after proving an a.e. statement on each source-cube image in a countable cover, it suffices to restrict from the countable union back to the target domain. No measurability hypothesis on the cover pieces is needed, because the statement is phrased directly with restricted measures.

theorem AleksandrovDifferentiability.affine_image_sourceOpenCube_subset_ball {n : ℕ} (c : SourceCubeSpace n) {r R ε : ℝ} (hr : 0 ≤ r) (hR : 0 ≤ R) (hsmall : √↑n * R * r < ε) : sourceAffineCubeImage n c r R ⊆ Metric.ball c ε

A scaled source cube of radius R sits in a metric ball when the scale is small enough.

This is the elementary geometric estimate behind the source localization step. It uses the explicit bound ‖z‖ ≤ sqrt n * R for z ∈ Q_R.

theorem AleksandrovDifferentiability.affine_image_sourceOpenCube_three_subset_ball {n : ℕ} (c : SourceCubeSpace n) {r ε : ℝ} (hr : 0 ≤ r) (hsmall : √↑n * 3 * r < ε) : sourceAffineCubeImage n c r 3 ⊆ Metric.ball c ε

A scaled source Q_3 sits in a metric ball when the scale is small enough.

theorem AleksandrovDifferentiability.exists_affine_sourceOpenCube_one_mem_and_outer_subset_of_isOpen {n : ℕ} {Ω : Set (SourceCubeSpace n)} (hΩ : IsOpen Ω) {x : SourceCubeSpace n} (hx : x ∈ Ω) {R : ℝ} (hR : 0 ≤ R) : ∃ (r : ℝ), 0 < r ∧ x ∈ sourceAffineCubeImage n x r 1 ∧ sourceAffineCubeImage n x r R ⊆ Ω

Pointwise source-cube localization inside an open set, with an arbitrary outer radius.

For every point of an open set and every nonnegative outer source radius R, there is a positive affine scale such that the image of Q_R stays inside the open set, while the point itself lies in the corresponding image of Q_1.

theorem AleksandrovDifferentiability.exists_affine_sourceOpenCube_one_mem_and_three_subset_of_isOpen {n : ℕ} {Ω : Set (SourceCubeSpace n)} (hΩ : IsOpen Ω) {x : SourceCubeSpace n} (hx : x ∈ Ω) : ∃ (r : ℝ), 0 < r ∧ x ∈ sourceAffineCubeImage n x r 1 ∧ sourceAffineCubeImage n x r 3 ⊆ Ω

Pointwise source-cube localization with outer radius 3.

theorem AleksandrovDifferentiability.exists_affine_sourceOpenCube_one_mem_and_four_subset_of_isOpen {n : ℕ} {Ω : Set (SourceCubeSpace n)} (hΩ : IsOpen Ω) {x : SourceCubeSpace n} (hx : x ∈ Ω) : ∃ (r : ℝ), 0 < r ∧ x ∈ sourceAffineCubeImage n x r 1 ∧ sourceAffineCubeImage n x r 4 ⊆ Ω

Pointwise source-cube localization with outer radius 4.

This is the variant used for open-domain localization, because Q_4 inside Ω leaves compact room for the closed Q_3 cube used to prove the boundedness hypothesis of the normalized source-cube theorem.

theorem AleksandrovDifferentiability.isOpen_sourceAffineCubeImage {n : ℕ} (a : SourceCubeSpace n) {r R : ℝ} (hr : r ≠ 0) : IsOpen (sourceAffineCubeImage n a r R)

Affine images of source open cubes are open when the scale is nonzero.

theorem AleksandrovDifferentiability.exists_countable_sourceAffineCubeCoverIndex_of_isOpen {n : ℕ} {Ω : Set (SourceCubeSpace n)} (hΩ : IsOpen Ω) : ∃ (I : Set (SourceAffineCubeCoverIndex n Ω)), I.Countable ∧ Ω ⊆ ⋃ i ∈ I, sourceAffineCubeImage n (↑i).1 (↑i).2 1

Countable Lindelöf subcover by affine source cubes whose enlarged cubes stay in an open set.

The index type still records the actual centers and scales. This is the countability refinement of exists_affine_sourceOpenCube_one_mem_and_three_subset_of_isOpen; a later theorem can apply the one-cube a.e. result on each selected index and assemble them with secondOrderDifferentiableAEOn_of_subset_iUnion.

theorem AleksandrovDifferentiability.exists_countable_sourceAffineCompactCubeCoverIndex_of_isOpen {n : ℕ} {Ω : Set (SourceCubeSpace n)} (hΩ : IsOpen Ω) : ∃ (I : Set (SourceAffineCompactCubeCoverIndex n Ω)), I.Countable ∧ Ω ⊆ ⋃ i ∈ I, sourceAffineCubeImage n (↑i).1 (↑i).2 1

Countable Lindelöf subcover by compactly contained affine source cubes.

The selected Q_1 images cover Ω, while each selected index records the stronger inclusion a + r • Q_4 ⊆ Ω. This is the localization cover used for the final open-domain theorem, because it leaves room to bound the pullback on Q_3.

theorem AleksandrovDifferentiability.ConvexOn.comp_sourceAffineCube {n : ℕ} {Ω : Set (SourceCubeSpace n)} {u : SourceCubeSpace n → ℝ} (hu : ConvexOn ℝ Ω u) {a : SourceCubeSpace n} {r R : ℝ} (himage : sourceAffineCubeImage n a r R ⊆ Ω) : ConvexOn ℝ (sourceOpenCube n R) fun (y : SourceCubeSpace n) => u (a + r • y)

Convexity inherited by the affine pullback on a source cube.

theorem AleksandrovDifferentiability.SourceAffineCompactCubeCoverIndex.convexOn_pullback_sourceOpenCube_three {n : ℕ} {Ω : Set (SourceCubeSpace n)} {u : SourceCubeSpace n → ℝ} (i : SourceAffineCompactCubeCoverIndex n Ω) (hu : ConvexOn ℝ Ω u) : ConvexOn ℝ (sourceOpenCube n 3) fun (y : SourceCubeSpace n) => u ((↑i).1 + (↑i).2 • y)

Convexity inherited by the affine pullback on Q_3 from a compact-room index.

theorem AleksandrovDifferentiability.SourceAffineCompactCubeCoverIndex.mapsTo_closedCube_three {n : ℕ} {Ω : Set (SourceCubeSpace n)} (i : SourceAffineCompactCubeCoverIndex n Ω) : Set.MapsTo (fun (y : SourceCubeSpace n) => (↑i).1 + (↑i).2 • y) (sourceClosedCube n 3) Ω

The closed Q_3 pullback of a compact-room affine cube stays inside the open domain.

theorem AleksandrovDifferentiability.SourceAffineCompactCubeCoverIndex.continuousOn_pullback_sourceClosedCube_three {n : ℕ} {Ω : Set (SourceCubeSpace n)} {u : SourceCubeSpace n → ℝ} (i : SourceAffineCompactCubeCoverIndex n Ω) (hΩ : IsOpen Ω) (hu : ConvexOn ℝ Ω u) : ContinuousOn (fun (y : SourceCubeSpace n) => u ((↑i).1 + (↑i).2 • y)) (sourceClosedCube n 3)

Continuity inherited on the compact closed Q_3 from convexity on the open domain.

theorem AleksandrovDifferentiability.SourceAffineCompactCubeCoverIndex.boundedOn_pullback_sourceOpenCube_three {n : ℕ} {Ω : Set (SourceCubeSpace n)} {u : SourceCubeSpace n → ℝ} (i : SourceAffineCompactCubeCoverIndex n Ω) (hΩ : IsOpen Ω) (hu : ConvexOn ℝ Ω u) : BoundedOn (sourceOpenCube n 3) fun (y : SourceCubeSpace n) => u ((↑i).1 + (↑i).2 • y)

Boundedness on Q_3 inherited from compact containment in an open convex domain.

theorem AleksandrovDifferentiability.secondOrderDifferentiableAEOn_of_subset_iUnion {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {ι : Type u_2} [Countable ι] {μ : MeasureTheory.Measure E} {Ω : Set E} {U : ι → Set E} {u : E → ℝ} (hcover : Ω ⊆ ⋃ (i : ι), U i) (hU : ∀ (i : ι), SecondOrderDifferentiableAEOn μ (U i) u) : SecondOrderDifferentiableAEOn μ Ω u

Countable-cover assembly specialized to second-order differentiability.

theorem AleksandrovDifferentiability.measure_secondOrderBadSetOn_eq_zero_of_subset_iUnion {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {ι : Type u_2} [Countable ι] {μ : MeasureTheory.Measure E} {Ω : Set E} {U : ι → Set E} {u : E → ℝ} (hΩ : MeasurableSet Ω) (hcover : Ω ⊆ ⋃ (i : ι), U i) (hU : ∀ (i : ι), SecondOrderDifferentiableAEOn μ (U i) u) : μ (secondOrderBadSetOn Ω u) = 0

Null-bad-set version of secondOrderDifferentiableAEOn_of_subset_iUnion.

theorem AleksandrovDifferentiability.map_volume_add_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (a : E) {r : ℝ} (hr : r ≠ 0) : MeasureTheory.Measure.map (fun (z : E) => a + r • z) MeasureTheory.volume = ENNReal.ofReal |(r ^ Module.finrank ℝ E)⁻¹| • MeasureTheory.volume

Lebesgue measure is scaled by a nonzero scalar dilation and unchanged by translation.

theorem AleksandrovDifferentiability.restrict_map_volume_add_smul_image {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (a : E) {r : ℝ} (hr : r ≠ 0) (s : Set E) : (MeasureTheory.Measure.map (fun (z : E) => a + r • z) MeasureTheory.volume).restrict ((fun (z : E) => a + r • z) '' s) = ENNReal.ofReal |(r ^ Module.finrank ℝ E)⁻¹| • MeasureTheory.volume.restrict ((fun (z : E) => a + r • z) '' s)

Restricted version of map_volume_add_smul on an affine image.

theorem AleksandrovDifferentiability.ae_map_add_smul_secondOrderDifferentiableAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {u : E → ℝ} {a : E} {r : ℝ} (hr : r ≠ 0) {μ : MeasureTheory.Measure E} (h : ∀ᵐ (z : E) ∂μ, SecondOrderDifferentiableAt (fun (y : E) => u (a + r • y)) z) : ∀ᵐ (x : E) ∂MeasureTheory.Measure.map (fun (z : E) => a + r • z) μ, SecondOrderDifferentiableAt u x

Push a.e. second-order differentiability through a nonzero scalar dilation and translation.

This is the measure-level form of the source localization map z ↦ a + r z. It does not yet identify the pushforward measure with Lebesgue measure on the affine image of the source cube; that is the next measure-transport component of the open-domain localization proof.

theorem AleksandrovDifferentiability.ae_restrict_image_add_smul_secondOrderDifferentiableAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {u : E → ℝ} {a : E} {r : ℝ} (hr : r ≠ 0) {μ : MeasureTheory.Measure E} {s : Set E} (h : ∀ᵐ (z : E) ∂μ.restrict s, SecondOrderDifferentiableAt (fun (y : E) => u (a + r • y)) z) : ∀ᵐ (x : E) ∂(MeasureTheory.Measure.map (fun (z : E) => a + r • z) μ).restrict ((fun (z : E) => a + r • z) '' s), SecondOrderDifferentiableAt u x

Restricted-image version of ae_map_add_smul_secondOrderDifferentiableAt.

If the pullback is second-order differentiable a.e. on s, then u is second-order differentiable a.e. on the affine image of s, measured using the pushforward of μ restricted to that image.

theorem AleksandrovDifferentiability.ae_restrict_affineImage_sourceOpenCube_secondOrderDifferentiableAt {n : ℕ} (hn : 1 ≤ n) {u : SourceCubeSpace n → ℝ} {a : SourceCubeSpace n} {r : ℝ} (hr : r ≠ 0) (hbounded : BoundedOn (sourceOpenCube n 3) fun (y : SourceCubeSpace n) => u (a + r • y)) (hconvex : ConvexOn ℝ (sourceOpenCube n 3) fun (y : SourceCubeSpace n) => u (a + r • y)) : ∀ᵐ (x : SourceCubeSpace n) ∂(MeasureTheory.Measure.map (fun (z : SourceCubeSpace n) => a + r • z) MeasureTheory.volume).restrict ((fun (z : SourceCubeSpace n) => a + r • z) '' sourceOpenCube n 1), SecondOrderDifferentiableAt u x

One-cube affine-image localization of the normalized source-cube theorem.

For a fixed affine map z ↦ a + r • z, if the pullback satisfies the boundedness and convexity hypotheses of the normalized theorem on Q_3, then u is second-order differentiable a.e. on the affine image of Q_1, measured by the restricted pushforward of Lebesgue measure.

theorem AleksandrovDifferentiability.ae_volume_restrict_affineImage_sourceOpenCube_secondOrderDifferentiableAt {n : ℕ} (hn : 1 ≤ n) {u : SourceCubeSpace n → ℝ} {a : SourceCubeSpace n} {r : ℝ} (hr : r ≠ 0) (hbounded : BoundedOn (sourceOpenCube n 3) fun (y : SourceCubeSpace n) => u (a + r • y)) (hconvex : ConvexOn ℝ (sourceOpenCube n 3) fun (y : SourceCubeSpace n) => u (a + r • y)) : ∀ᵐ (x : SourceCubeSpace n) ∂MeasureTheory.volume.restrict ((fun (z : SourceCubeSpace n) => a + r • z) '' sourceOpenCube n 1), SecondOrderDifferentiableAt u x

One-cube affine-image localization with Lebesgue measure restricted to the affine image.

theorem AleksandrovDifferentiability.SourceAffineCompactCubeCoverIndex.ae_volume_restrict_image_secondOrderDifferentiableAt {n : ℕ} (hn : 1 ≤ n) {Ω : Set (SourceCubeSpace n)} {u : SourceCubeSpace n → ℝ} (i : SourceAffineCompactCubeCoverIndex n Ω) (hΩ : IsOpen Ω) (hu : ConvexOn ℝ Ω u) : ∀ᵐ (x : SourceCubeSpace n) ∂MeasureTheory.volume.restrict (sourceAffineCubeImage n (↑i).1 (↑i).2 1), SecondOrderDifferentiableAt u x

One selected compact-room affine cube satisfies the Lebesgue-restricted a.e. conclusion.

theorem AleksandrovDifferentiability.ae_volume_restrict_open_secondOrderDifferentiableAt_sourceCubeSpace {n : ℕ} (hn : 1 ≤ n) {Ω : Set (SourceCubeSpace n)} {u : SourceCubeSpace n → ℝ} (hΩ : IsOpen Ω) (hu : ConvexOn ℝ Ω u) : ∀ᵐ (x : SourceCubeSpace n) ∂MeasureTheory.volume.restrict Ω, SecondOrderDifferentiableAt u x

Open-domain localization in source-cube coordinates.

This is the source's cube-to-open-domain localization step in the positive-dimensional source coordinate model: cover the open domain by countably many compact-room affine Q_1 images, apply the normalized theorem on each image, and assemble the restricted a.e. conclusions.

theorem AleksandrovDifferentiability.convexAleksandrovAEStatement_sourceCubeSpace_of_one_le {n : ℕ} (hn : 1 ≤ n) (Ω : Set (SourceCubeSpace n)) (u : SourceCubeSpace n → ℝ) : ConvexAleksandrovAEStatement (SourceCubeSpace n) Ω u

Positive-dimensional source-coordinate version of the convex Aleksandrov a.e. statement.

theorem AleksandrovDifferentiability.convexAleksandrovAEStatement_finiteDimensional (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (Ω : Set E) (u : E → ℝ) : ConvexAleksandrovAEStatement E Ω u

Full finite-dimensional convex Aleksandrov a.e. statement, obtained from the source-coordinate localization theorem by an orthonormal-coordinate linear isometry equivalence.