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

Good and bad sets for second-order differentiability #

This file gives names to the full-measure and exceptional-set formulations of the final second-order differentiability conclusion.

source

theorem AleksandrovDifferentiability.prod_measure_diff_eq_zero_of_ae_ae_restrict_section {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s G : Set (α × β)} (hs : MeasurableSet s) (hbad : MeasurableSet (s \ G)) (hsection : ∀ᵐ (x : α) ∂μ, ∀ᵐ (y : β) ∂ν.restrict {y : β | (x, y) ∈ s}, (x, y) ∈ G) :

(μ.prod ν) (s \ G) = 0

Product-measure Fubini bookkeeping for a.e. restricted vertical sections.

If almost every vertical section of s is almost everywhere contained in G, measured with respect to the restriction of ν to that section, then the product-measure complement s \ G is null. This is the set-level shape needed later when a one-dimensional line theorem is integrated over transverse coordinates.

source

theorem AleksandrovDifferentiability.prod_measure_diff_eq_zero_of_ae_ae_restrict_section₀ {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s G : Set (α × β)} (hs : MeasurableSet s) (hbad : MeasureTheory.NullMeasurableSet (s \ G) (μ.prod ν)) (hsection : ∀ᵐ (x : α) ∂μ, ∀ᵐ (y : β) ∂ν.restrict {y : β | (x, y) ∈ s}, (x, y) ∈ G) :

(μ.prod ν) (s \ G) = 0

Null-measurable version of prod_measure_diff_eq_zero_of_ae_ae_restrict_section.

This weakens the side condition on the product bad set from measurable to null-measurable, which is often the natural output when the one-dimensional good set is only known modulo null sets.

source

theorem AleksandrovDifferentiability.prod_measure_diff_eq_zero_of_forall_ae_restrict_section {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s G : Set (α × β)} (hs : MeasurableSet s) (hbad : MeasurableSet (s \ G)) (hsection : ∀ (x : α), ∀ᵐ (y : β) ∂ν.restrict {y : β | (x, y) ∈ s}, (x, y) ∈ G) :

(μ.prod ν) (s \ G) = 0

Product-measure Fubini bookkeeping for restricted vertical sections.

If every vertical section of s is almost everywhere contained in G, measured with respect to the restriction of ν to that section, then the product-measure complement s \ G is null.

source

theorem AleksandrovDifferentiability.prod_measure_diff_eq_zero_of_forall_ae_restrict_section₀ {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s G : Set (α × β)} (hs : MeasurableSet s) (hbad : MeasureTheory.NullMeasurableSet (s \ G) (μ.prod ν)) (hsection : ∀ (x : α), ∀ᵐ (y : β) ∂ν.restrict {y : β | (x, y) ∈ s}, (x, y) ∈ G) :

(μ.prod ν) (s \ G) = 0

Null-measurable version of prod_measure_diff_eq_zero_of_forall_ae_restrict_section.

source

theorem AleksandrovDifferentiability.prod_measure_diff_eq_zero_of_ae_ae_imp {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s G : Set (α × β)} (hs : MeasurableSet s) (hbad : MeasurableSet (s \ G)) (hsection : ∀ᵐ (x : α) ∂μ, ∀ᵐ (y : β) ∂ν, (x, y) ∈ s → (x, y) ∈ G) :

(μ.prod ν) (s \ G) = 0

Product-measure Fubini bookkeeping for restricted vertical sections in implication form.

source

theorem AleksandrovDifferentiability.prod_measure_diff_eq_zero_of_ae_ae_imp₀ {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s G : Set (α × β)} (hs : MeasurableSet s) (hbad : MeasureTheory.NullMeasurableSet (s \ G) (μ.prod ν)) (hsection : ∀ᵐ (x : α) ∂μ, ∀ᵐ (y : β) ∂ν, (x, y) ∈ s → (x, y) ∈ G) :

(μ.prod ν) (s \ G) = 0

Null-measurable version of prod_measure_diff_eq_zero_of_ae_ae_imp.

source

theorem AleksandrovDifferentiability.prod_measure_diff_eq_zero_of_forall_ae_imp {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s G : Set (α × β)} (hs : MeasurableSet s) (hbad : MeasurableSet (s \ G)) (hsection : ∀ (x : α), ∀ᵐ (y : β) ∂ν, (x, y) ∈ s → (x, y) ∈ G) :

(μ.prod ν) (s \ G) = 0

Product-measure Fubini bookkeeping for restricted vertical sections in pointwise implication form.

source

theorem AleksandrovDifferentiability.prod_measure_diff_eq_zero_of_forall_ae_imp₀ {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s G : Set (α × β)} (hs : MeasurableSet s) (hbad : MeasureTheory.NullMeasurableSet (s \ G) (μ.prod ν)) (hsection : ∀ (x : α), ∀ᵐ (y : β) ∂ν, (x, y) ∈ s → (x, y) ∈ G) :

(μ.prod ν) (s \ G) = 0

Null-measurable version of prod_measure_diff_eq_zero_of_forall_ae_imp.

source

theorem AleksandrovDifferentiability.prod_measure_diff_eq_zero_of_ae_ae_restrict_horizontal_section {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {s G : Set (α × β)} (hs : MeasurableSet s) (hbad : MeasurableSet (s \ G)) (hsection : ∀ᵐ (y : β) ∂ν, ∀ᵐ (x : α) ∂μ.restrict {x : α | (x, y) ∈ s}, (x, y) ∈ G) :

(μ.prod ν) (s \ G) = 0

Product-measure Fubini bookkeeping for a.e. restricted horizontal sections.

This is the coordinate-swapped version of prod_measure_diff_eq_zero_of_ae_ae_restrict_section: if almost every horizontal section of s is almost everywhere contained in G, measured with respect to the restriction of μ to that section, then the product-measure complement s \ G is null.

source

theorem AleksandrovDifferentiability.prod_measure_diff_eq_zero_of_ae_ae_restrict_horizontal_section₀ {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {s G : Set (α × β)} (hs : MeasurableSet s) (hbad : MeasureTheory.NullMeasurableSet (s \ G) (μ.prod ν)) (hsection : ∀ᵐ (y : β) ∂ν, ∀ᵐ (x : α) ∂μ.restrict {x : α | (x, y) ∈ s}, (x, y) ∈ G) :

(μ.prod ν) (s \ G) = 0

Null-measurable version of prod_measure_diff_eq_zero_of_ae_ae_restrict_horizontal_section.

source

theorem AleksandrovDifferentiability.prod_measure_diff_eq_zero_of_forall_ae_restrict_horizontal_section {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {s G : Set (α × β)} (hs : MeasurableSet s) (hbad : MeasurableSet (s \ G)) (hsection : ∀ (y : β), ∀ᵐ (x : α) ∂μ.restrict {x : α | (x, y) ∈ s}, (x, y) ∈ G) :

(μ.prod ν) (s \ G) = 0

Product-measure Fubini bookkeeping for restricted horizontal sections.

If every horizontal section of s is almost everywhere contained in G, measured with respect to the restriction of μ to that section, then the product-measure complement s \ G is null.

source

theorem AleksandrovDifferentiability.prod_measure_diff_eq_zero_of_forall_ae_restrict_horizontal_section₀ {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {s G : Set (α × β)} (hs : MeasurableSet s) (hbad : MeasureTheory.NullMeasurableSet (s \ G) (μ.prod ν)) (hsection : ∀ (y : β), ∀ᵐ (x : α) ∂μ.restrict {x : α | (x, y) ∈ s}, (x, y) ∈ G) :

(μ.prod ν) (s \ G) = 0

Null-measurable version of prod_measure_diff_eq_zero_of_forall_ae_restrict_horizontal_section.

source

theorem AleksandrovDifferentiability.prod_measure_diff_eq_zero_of_ae_ae_horizontal_imp {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {s G : Set (α × β)} (hs : MeasurableSet s) (hbad : MeasurableSet (s \ G)) (hsection : ∀ᵐ (y : β) ∂ν, ∀ᵐ (x : α) ∂μ, (x, y) ∈ s → (x, y) ∈ G) :

(μ.prod ν) (s \ G) = 0

Product-measure Fubini bookkeeping for restricted horizontal sections in implication form.

source

theorem AleksandrovDifferentiability.prod_measure_diff_eq_zero_of_ae_ae_horizontal_imp₀ {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {s G : Set (α × β)} (hs : MeasurableSet s) (hbad : MeasureTheory.NullMeasurableSet (s \ G) (μ.prod ν)) (hsection : ∀ᵐ (y : β) ∂ν, ∀ᵐ (x : α) ∂μ, (x, y) ∈ s → (x, y) ∈ G) :

(μ.prod ν) (s \ G) = 0

Null-measurable version of prod_measure_diff_eq_zero_of_ae_ae_horizontal_imp.

source

theorem AleksandrovDifferentiability.prod_measure_diff_eq_zero_of_forall_ae_horizontal_imp {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {s G : Set (α × β)} (hs : MeasurableSet s) (hbad : MeasurableSet (s \ G)) (hsection : ∀ (y : β), ∀ᵐ (x : α) ∂μ, (x, y) ∈ s → (x, y) ∈ G) :

(μ.prod ν) (s \ G) = 0

Product-measure Fubini bookkeeping for restricted horizontal sections in pointwise implication form.

source

theorem AleksandrovDifferentiability.prod_measure_diff_eq_zero_of_forall_ae_horizontal_imp₀ {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {s G : Set (α × β)} (hs : MeasurableSet s) (hbad : MeasureTheory.NullMeasurableSet (s \ G) (μ.prod ν)) (hsection : ∀ (y : β), ∀ᵐ (x : α) ∂μ, (x, y) ∈ s → (x, y) ∈ G) :

(μ.prod ν) (s \ G) = 0

Null-measurable version of prod_measure_diff_eq_zero_of_forall_ae_horizontal_imp.

source

def AleksandrovDifferentiability.secondOrderBadSet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ) :

Set E

The exceptional set where u is not second-order differentiable.

Equations

AleksandrovDifferentiability.secondOrderBadSet u = (AleksandrovDifferentiability.secondOrderDifferentiabilitySet u)ᶜ

Instances For

source

def AleksandrovDifferentiability.secondOrderBadSetOn {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (s : Set E) (u : E → ℝ) :

Set E

The exceptional set inside a prescribed domain.

Equations

AleksandrovDifferentiability.secondOrderBadSetOn s u = s \ AleksandrovDifferentiability.secondOrderDifferentiabilitySet u

Instances For

source

@[simp]

theorem AleksandrovDifferentiability.mem_secondOrderBadSet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x : E} :

x ∈ secondOrderBadSet u ↔ ¬SecondOrderDifferentiableAt u x

source

@[simp]

theorem AleksandrovDifferentiability.mem_secondOrderBadSetOn {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} :

x ∈ secondOrderBadSetOn s u ↔ x ∈ s ∧ ¬SecondOrderDifferentiableAt u x

source

def AleksandrovDifferentiability.SecondOrderDifferentiableAE {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] (μ : MeasureTheory.Measure E) (u : E → ℝ) :

Prop

u is second-order differentiable almost everywhere with respect to μ.

Equations

AleksandrovDifferentiability.SecondOrderDifferentiableAE μ u = ∀ᵐ (x : E) ∂μ, AleksandrovDifferentiability.SecondOrderDifferentiableAt u x

Instances For

source

def AleksandrovDifferentiability.SecondOrderDifferentiableAEOn {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] (μ : MeasureTheory.Measure E) (s : Set E) (u : E → ℝ) :

Prop

u is second-order differentiable almost everywhere on s, with respect to μ.

Equations

AleksandrovDifferentiability.SecondOrderDifferentiableAEOn μ s u = ∀ᵐ (x : E) ∂μ.restrict s, AleksandrovDifferentiability.SecondOrderDifferentiableAt u x

Instances For

source

theorem AleksandrovDifferentiability.secondOrderDifferentiableAE_iff_measure_secondOrderBadSet_eq_zero {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {u : E → ℝ} :

SecondOrderDifferentiableAE μ u ↔ μ (secondOrderBadSet u) = 0

source

theorem AleksandrovDifferentiability.secondOrderDifferentiableAEOn_iff_restrict_measure_secondOrderBadSet_eq_zero {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} :

SecondOrderDifferentiableAEOn μ s u ↔ (μ.restrict s) (secondOrderBadSet u) = 0

source

theorem AleksandrovDifferentiability.restrict_measure_secondOrderBadSet_eq_zero_of_secondOrderDifferentiableAEOn {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (h : SecondOrderDifferentiableAEOn μ s u) :

(μ.restrict s) (secondOrderBadSet u) = 0

Restricted-measure null-bad-set form of an a.e.-on statement.

source

theorem AleksandrovDifferentiability.secondOrderDifferentiableAEOn_of_restrict_measure_secondOrderBadSet_eq_zero {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (h : (μ.restrict s) (secondOrderBadSet u) = 0) :

SecondOrderDifferentiableAEOn μ s u

A restricted-measure null bad set gives second-order differentiability a.e. on the domain.

source

theorem AleksandrovDifferentiability.secondOrderBadSet_inter_eq_secondOrderBadSetOn {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} :

secondOrderBadSet u ∩ s = secondOrderBadSetOn s u

source

theorem AleksandrovDifferentiability.secondOrderDifferentiableAEOn_iff_measure_secondOrderBadSetOn_eq_zero {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (hs : MeasurableSet s) :

SecondOrderDifferentiableAEOn μ s u ↔ μ (secondOrderBadSetOn s u) = 0

source

theorem AleksandrovDifferentiability.secondOrderBadSetOn_subset_domain {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} :

secondOrderBadSetOn s u ⊆ s

source

theorem AleksandrovDifferentiability.measure_secondOrderBadSetOn_eq_zero_of_measure_eq_zero {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (hs0 : μ s = 0) :

μ (secondOrderBadSetOn s u) = 0

source

theorem AleksandrovDifferentiability.secondOrderDifferentiableAEOn_of_measure_eq_zero {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (hs : MeasurableSet s) (hs0 : μ s = 0) :

SecondOrderDifferentiableAEOn μ s u

source

@[simp]

theorem AleksandrovDifferentiability.secondOrderBadSetOn_empty {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} :

secondOrderBadSetOn ∅ u = ∅

source

theorem AleksandrovDifferentiability.secondOrderDifferentiableAEOn_empty {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {u : E → ℝ} :

SecondOrderDifferentiableAEOn μ ∅ u

source

theorem AleksandrovDifferentiability.secondOrderDifferentiableAEOn_of_secondOrderBadSetOn_subset_null {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} {N : Set E} (hs : MeasurableSet s) (hsubset : secondOrderBadSetOn s u ⊆ N) (hN : μ N = 0) :

SecondOrderDifferentiableAEOn μ s u

source

theorem AleksandrovDifferentiability.secondOrderBadSetOn_subset_domain_diff_of_inter_subset_differentiabilitySet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s G : Set E} {u : E → ℝ} (hG : s ∩ G ⊆ secondOrderDifferentiabilitySet u) :

secondOrderBadSetOn s u ⊆ s \ G

source

theorem AleksandrovDifferentiability.secondOrderDifferentiableAEOn_of_fullMeasure_goodSet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s G : Set E} {u : E → ℝ} (hs : MeasurableSet s) (hnull : μ (s \ G) = 0) (hG : s ∩ G ⊆ secondOrderDifferentiabilitySet u) :

SecondOrderDifferentiableAEOn μ s u

source

theorem AleksandrovDifferentiability.secondOrderDifferentiableAEOn_of_fullMeasure_goodSet' {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s G : Set E} {u : E → ℝ} (hs : MeasurableSet s) (hnull : μ (s \ G) = 0) (hG : ∀ ⦃x : E⦄, x ∈ s → x ∈ G → SecondOrderDifferentiableAt u x) :

SecondOrderDifferentiableAEOn μ s u

source

theorem AleksandrovDifferentiability.secondOrderDifferentiableAEOn_of_forall_mem {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (hs : MeasurableSet s) (h : ∀ ⦃x : E⦄, x ∈ s → SecondOrderDifferentiableAt u x) :

SecondOrderDifferentiableAEOn μ s u

If every point of s is second-order differentiable, then u is second-order differentiable almost everywhere on s. This is the degenerate good-set case G = s.

source

theorem AleksandrovDifferentiability.measure_secondOrderBadSetOn_eq_zero_of_forall_mem {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (hs : MeasurableSet s) (h : ∀ ⦃x : E⦄, x ∈ s → SecondOrderDifferentiableAt u x) :

μ (secondOrderBadSetOn s u) = 0

Null-bad-set version of secondOrderDifferentiableAEOn_of_forall_mem.

source

theorem AleksandrovDifferentiability.restrict_measure_secondOrderBadSet_eq_zero_of_forall_mem {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (hs : MeasurableSet s) (h : ∀ ⦃x : E⦄, x ∈ s → SecondOrderDifferentiableAt u x) :

(μ.restrict s) (secondOrderBadSet u) = 0

Restricted-measure null-bad-set version of secondOrderDifferentiableAEOn_of_forall_mem.

source

theorem AleksandrovDifferentiability.secondOrderDifferentiableAEOn_of_forall_expansionData {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (hs : MeasurableSet s) (h : ∀ ⦃x : E⦄, x ∈ s → ∃ (p : E) (B : E →L[ℝ ] E), IsSymmetricOperator B ∧ HasSecondOrderExpansionAt u x p B) :

SecondOrderDifferentiableAEOn μ s u

If every point of s carries explicit symmetric second-order expansion data, then u is second-order differentiable almost everywhere on s.

source

theorem AleksandrovDifferentiability.measure_secondOrderBadSetOn_eq_zero_of_forall_expansionData {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (hs : MeasurableSet s) (h : ∀ ⦃x : E⦄, x ∈ s → ∃ (p : E) (B : E →L[ℝ ] E), IsSymmetricOperator B ∧ HasSecondOrderExpansionAt u x p B) :

μ (secondOrderBadSetOn s u) = 0

Null-bad-set version of secondOrderDifferentiableAEOn_of_forall_expansionData.

source

theorem AleksandrovDifferentiability.restrict_measure_secondOrderBadSet_eq_zero_of_forall_expansionData {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (hs : MeasurableSet s) (h : ∀ ⦃x : E⦄, x ∈ s → ∃ (p : E) (B : E →L[ℝ ] E), IsSymmetricOperator B ∧ HasSecondOrderExpansionAt u x p B) :

(μ.restrict s) (secondOrderBadSet u) = 0

Restricted-measure null-bad-set version of secondOrderDifferentiableAEOn_of_forall_expansionData.

source

theorem AleksandrovDifferentiability.secondOrderDifferentiableAEOn_of_forall_clmExpansionData {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (hs : MeasurableSet s) (h : ∀ ⦃x : E⦄, x ∈ s → ∃ (p : E) (ℓ : E →L[ℝ ] ℝ) (B : E →L[ℝ ] E), (∀ (z : E), ℓ z = inner ℝ p z) ∧ IsSymmetricOperator B ∧ HasSecondOrderExpansionAtCLM u x ℓ B) :

SecondOrderDifferentiableAEOn μ s u

If every point of s carries explicit symmetric second-order expansion data with the first-order term given as a represented continuous linear functional, then u is second-order differentiable almost everywhere on s.

source

theorem AleksandrovDifferentiability.measure_secondOrderBadSetOn_eq_zero_of_forall_clmExpansionData {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (hs : MeasurableSet s) (h : ∀ ⦃x : E⦄, x ∈ s → ∃ (p : E) (ℓ : E →L[ℝ ] ℝ) (B : E →L[ℝ ] E), (∀ (z : E), ℓ z = inner ℝ p z) ∧ IsSymmetricOperator B ∧ HasSecondOrderExpansionAtCLM u x ℓ B) :

μ (secondOrderBadSetOn s u) = 0

Null-bad-set version of secondOrderDifferentiableAEOn_of_forall_clmExpansionData.

source

theorem AleksandrovDifferentiability.restrict_measure_secondOrderBadSet_eq_zero_of_forall_clmExpansionData {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} (hs : MeasurableSet s) (h : ∀ ⦃x : E⦄, x ∈ s → ∃ (p : E) (ℓ : E →L[ℝ ] ℝ) (B : E →L[ℝ ] E), (∀ (z : E), ℓ z = inner ℝ p z) ∧ IsSymmetricOperator B ∧ HasSecondOrderExpansionAtCLM u x ℓ B) :

(μ.restrict s) (secondOrderBadSet u) = 0

Restricted-measure null-bad-set version of secondOrderDifferentiableAEOn_of_forall_clmExpansionData.

source

theorem AleksandrovDifferentiability.ae_restrict_mem_of_measure_diff_eq_zero {E : Type u_1} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s G : Set E} (hs : MeasurableSet s) (hnull : μ (s \ G) = 0) :

∀ᵐ (x : E) ∂μ.restrict s, x ∈ G

If G has full measure inside s, then almost every point of s, for the restricted measure, belongs to G. This version does not require measurability of G.

source

theorem AleksandrovDifferentiability.measure_diff_eq_zero_of_ae_restrict_mem {E : Type u_1} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s G : Set E} (hs : MeasurableSet s) (hmem : ∀ᵐ (x : E) ∂μ.restrict s, x ∈ G) :

μ (s \ G) = 0

A.e. membership in G for the restricted measure is the same as G having null complement inside s. This version does not require measurability of G.

source

theorem AleksandrovDifferentiability.secondOrderDifferentiableAEOn_of_ae_goodSet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s G : Set E} {u : E → ℝ} (hs : MeasurableSet s) (hmem : ∀ᵐ (x : E) ∂μ.restrict s, x ∈ G) (hG : ∀ ⦃x : E⦄, x ∈ s → x ∈ G → SecondOrderDifferentiableAt u x) :

SecondOrderDifferentiableAEOn μ s u

A.e. membership version of secondOrderDifferentiableAEOn_of_fullMeasure_goodSet'. This is convenient for Fubini arguments that naturally produce restricted-a.e. membership rather than a null-complement statement.

source

theorem AleksandrovDifferentiability.measure_diff_eq_zero_of_subset_of_measure_diff_eq_zero {E : Type u_1} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s G H : Set E} (hGH : G ⊆ H) (hG : μ (s \ G) = 0) :

μ (s \ H) = 0

Full-measure-in-s is monotone when the good set is enlarged.

source

theorem AleksandrovDifferentiability.ae_restrict_mem_iInter_of_forall_measure_diff_eq_zero {E : Type u_1} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {G : ℕ → Set E} (hs : MeasurableSet s) (hnull : ∀ (n : ℕ), μ (s \ G n) = 0) :

∀ᵐ (x : E) ∂μ.restrict s, x ∈ ⋂ (n : ℕ), G n

Countably many full-measure subsets of s hold simultaneously almost everywhere on s. This is the main bookkeeping lemma for intersections of line/density good sets.

source

theorem AleksandrovDifferentiability.secondOrderDifferentiableAEOn_of_countable_fullMeasure_goodSets {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {G : ℕ → Set E} {u : E → ℝ} (hs : MeasurableSet s) (hnull : ∀ (n : ℕ), μ (s \ G n) = 0) (hG : ∀ ⦃x : E⦄, x ∈ s → (∀ (n : ℕ), x ∈ G n) → SecondOrderDifferentiableAt u x) :

SecondOrderDifferentiableAEOn μ s u

If countably many full-measure good sets jointly imply second-order differentiability on s, then u is second-order differentiable almost everywhere on s.

source

theorem AleksandrovDifferentiability.secondOrderDifferentiableAEOn_of_countable_fullMeasure_expansionData {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {G : ℕ → Set E} {u : E → ℝ} (hs : MeasurableSet s) (hnull : ∀ (n : ℕ), μ (s \ G n) = 0) (hG : ∀ ⦃x : E⦄, x ∈ s → (∀ (n : ℕ), x ∈ G n) → ∃ (p : E) (B : E →L[ℝ ] E), IsSymmetricOperator B ∧ HasSecondOrderExpansionAt u x p B) :

SecondOrderDifferentiableAEOn μ s u

Countable full-measure good sets whose simultaneous validity gives explicit symmetric second-order expansion data imply second-order differentiability almost everywhere on s.

source

theorem AleksandrovDifferentiability.secondOrderDifferentiableAEOn_of_countable_fullMeasure_clmExpansionData {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {G : ℕ → Set E} {u : E → ℝ} (hs : MeasurableSet s) (hnull : ∀ (n : ℕ), μ (s \ G n) = 0) (hG : ∀ ⦃x : E⦄, x ∈ s → (∀ (n : ℕ), x ∈ G n) → ∃ (p : E) (ℓ : E →L[ℝ ] ℝ) (B : E →L[ℝ ] E), (∀ (z : E), ℓ z = inner ℝ p z) ∧ IsSymmetricOperator B ∧ HasSecondOrderExpansionAtCLM u x ℓ B) :

SecondOrderDifferentiableAEOn μ s u

Countable full-measure good sets whose simultaneous validity gives represented continuous-linear first-order expansion data imply second-order differentiability almost everywhere on s.

source

theorem AleksandrovDifferentiability.secondOrderDifferentiabilitySet_eq_setOf_exists_expansionData {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} :

secondOrderDifferentiabilitySet u = {x : E | ∃ (p : E) (B : E →L[ℝ ] E), IsSymmetricOperator B ∧ HasSecondOrderExpansionAt u x p B}

The differentiability locus is exactly the set of points carrying some symmetric second-order expansion data. This is mostly a named unfolding for final assembly arguments.

source

theorem AleksandrovDifferentiability.secondOrderDifferentiableAEOn_of_fullMeasure_expansionSet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {u : E → ℝ} {p : E} {B : E →L[ℝ ] E} (hs : MeasurableSet s) (hB : IsSymmetricOperator B) (hnull : μ (s \ secondOrderExpansionSet u p B) = 0) :

SecondOrderDifferentiableAEOn μ s u

If a fixed symmetric expansion locus has full measure in s, then u is second-order differentiable almost everywhere on s.

source

theorem AleksandrovDifferentiability.secondOrderDifferentiableAEOn_of_fullMeasure_expansionData {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s G : Set E} {u : E → ℝ} (hs : MeasurableSet s) (hnull : μ (s \ G) = 0) (hG : ∀ ⦃x : E⦄, x ∈ s → x ∈ G → ∃ (p : E) (B : E →L[ℝ ] E), IsSymmetricOperator B ∧ HasSecondOrderExpansionAt u x p B) :

SecondOrderDifferentiableAEOn μ s u

If a full-measure set in s carries explicit symmetric second-order expansion data at every point, then u is second-order differentiable almost everywhere on s.

source

theorem AleksandrovDifferentiability.secondOrderDifferentiableAEOn_of_fullMeasure_clmExpansionData {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s G : Set E} {u : E → ℝ} (hs : MeasurableSet s) (hnull : μ (s \ G) = 0) (hG : ∀ ⦃x : E⦄, x ∈ s → x ∈ G → ∃ (p : E) (ℓ : E →L[ℝ ] ℝ) (B : E →L[ℝ ] E), (∀ (z : E), ℓ z = inner ℝ p z) ∧ IsSymmetricOperator B ∧ HasSecondOrderExpansionAtCLM u x ℓ B) :

SecondOrderDifferentiableAEOn μ s u

If a full-measure set in s carries represented continuous-linear first-order expansion data at every point, then u is second-order differentiable almost everywhere on s.

source

theorem AleksandrovDifferentiability.measure_secondOrderBadSetOn_eq_zero_of_fullMeasure_expansionData {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s G : Set E} {u : E → ℝ} (hs : MeasurableSet s) (hnull : μ (s \ G) = 0) (hG : ∀ ⦃x : E⦄, x ∈ s → x ∈ G → ∃ (p : E) (B : E →L[ℝ ] E), IsSymmetricOperator B ∧ HasSecondOrderExpansionAt u x p B) :

μ (secondOrderBadSetOn s u) = 0

Null-bad-set version of secondOrderDifferentiableAEOn_of_fullMeasure_expansionData.

source

theorem AleksandrovDifferentiability.restrict_measure_secondOrderBadSet_eq_zero_of_fullMeasure_expansionData {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s G : Set E} {u : E → ℝ} (hs : MeasurableSet s) (hnull : μ (s \ G) = 0) (hG : ∀ ⦃x : E⦄, x ∈ s → x ∈ G → ∃ (p : E) (B : E →L[ℝ ] E), IsSymmetricOperator B ∧ HasSecondOrderExpansionAt u x p B) :

(μ.restrict s) (secondOrderBadSet u) = 0

Restricted-measure null-bad-set version of secondOrderDifferentiableAEOn_of_fullMeasure_expansionData.

source

theorem AleksandrovDifferentiability.measure_secondOrderBadSetOn_eq_zero_of_fullMeasure_clmExpansionData {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s G : Set E} {u : E → ℝ} (hs : MeasurableSet s) (hnull : μ (s \ G) = 0) (hG : ∀ ⦃x : E⦄, x ∈ s → x ∈ G → ∃ (p : E) (ℓ : E →L[ℝ ] ℝ) (B : E →L[ℝ ] E), (∀ (z : E), ℓ z = inner ℝ p z) ∧ IsSymmetricOperator B ∧ HasSecondOrderExpansionAtCLM u x ℓ B) :

μ (secondOrderBadSetOn s u) = 0

Null-bad-set version of secondOrderDifferentiableAEOn_of_fullMeasure_clmExpansionData.

source

theorem AleksandrovDifferentiability.restrict_measure_secondOrderBadSet_eq_zero_of_fullMeasure_clmExpansionData {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s G : Set E} {u : E → ℝ} (hs : MeasurableSet s) (hnull : μ (s \ G) = 0) (hG : ∀ ⦃x : E⦄, x ∈ s → x ∈ G → ∃ (p : E) (ℓ : E →L[ℝ ] ℝ) (B : E →L[ℝ ] E), (∀ (z : E), ℓ z = inner ℝ p z) ∧ IsSymmetricOperator B ∧ HasSecondOrderExpansionAtCLM u x ℓ B) :

(μ.restrict s) (secondOrderBadSet u) = 0

Restricted-measure null-bad-set version of secondOrderDifferentiableAEOn_of_fullMeasure_clmExpansionData.

source

theorem AleksandrovDifferentiability.measure_secondOrderBadSetOn_eq_zero_of_countable_fullMeasure_clmExpansionData {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {G : ℕ → Set E} {u : E → ℝ} (hs : MeasurableSet s) (hnull : ∀ (n : ℕ), μ (s \ G n) = 0) (hG : ∀ ⦃x : E⦄, x ∈ s → (∀ (n : ℕ), x ∈ G n) → ∃ (p : E) (ℓ : E →L[ℝ ] ℝ) (B : E →L[ℝ ] E), (∀ (z : E), ℓ z = inner ℝ p z) ∧ IsSymmetricOperator B ∧ HasSecondOrderExpansionAtCLM u x ℓ B) :

μ (secondOrderBadSetOn s u) = 0

Null-bad-set version of secondOrderDifferentiableAEOn_of_countable_fullMeasure_clmExpansionData.

source

theorem AleksandrovDifferentiability.restrict_measure_secondOrderBadSet_eq_zero_of_countable_fullMeasure_clmExpansionData {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {G : ℕ → Set E} {u : E → ℝ} (hs : MeasurableSet s) (hnull : ∀ (n : ℕ), μ (s \ G n) = 0) (hG : ∀ ⦃x : E⦄, x ∈ s → (∀ (n : ℕ), x ∈ G n) → ∃ (p : E) (ℓ : E →L[ℝ ] ℝ) (B : E →L[ℝ ] E), (∀ (z : E), ℓ z = inner ℝ p z) ∧ IsSymmetricOperator B ∧ HasSecondOrderExpansionAtCLM u x ℓ B) :

(μ.restrict s) (secondOrderBadSet u) = 0

Restricted-measure null-bad-set version of secondOrderDifferentiableAEOn_of_countable_fullMeasure_clmExpansionData.

source

theorem AleksandrovDifferentiability.secondOrderDifferentiableAEOn_of_forall_hilbertClmExpansionData {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [MeasurableSpace H] {μ : MeasureTheory.Measure H} {s : Set H} {u : H → ℝ} (hs : MeasurableSet s) (h : ∀ ⦃x : H⦄, x ∈ s → ∃ (ℓ : H →L[ℝ ] ℝ) (B : H →L[ℝ ] H), IsSymmetricOperator B ∧ HasSecondOrderExpansionAtCLM u x ℓ B) :

SecondOrderDifferentiableAEOn μ s u

In a real Hilbert space, pointwise CLM-gradient expansion data implies second-order differentiability almost everywhere on s.

source

theorem AleksandrovDifferentiability.measure_secondOrderBadSetOn_eq_zero_of_forall_hilbertClmExpansionData {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [MeasurableSpace H] {μ : MeasureTheory.Measure H} {s : Set H} {u : H → ℝ} (hs : MeasurableSet s) (h : ∀ ⦃x : H⦄, x ∈ s → ∃ (ℓ : H →L[ℝ ] ℝ) (B : H →L[ℝ ] H), IsSymmetricOperator B ∧ HasSecondOrderExpansionAtCLM u x ℓ B) :

μ (secondOrderBadSetOn s u) = 0

Null-bad-set version of secondOrderDifferentiableAEOn_of_forall_hilbertClmExpansionData.

source

theorem AleksandrovDifferentiability.restrict_measure_secondOrderBadSet_eq_zero_of_forall_hilbertClmExpansionData {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [MeasurableSpace H] {μ : MeasureTheory.Measure H} {s : Set H} {u : H → ℝ} (hs : MeasurableSet s) (h : ∀ ⦃x : H⦄, x ∈ s → ∃ (ℓ : H →L[ℝ ] ℝ) (B : H →L[ℝ ] H), IsSymmetricOperator B ∧ HasSecondOrderExpansionAtCLM u x ℓ B) :

(μ.restrict s) (secondOrderBadSet u) = 0

Restricted-measure null-bad-set version of secondOrderDifferentiableAEOn_of_forall_hilbertClmExpansionData.

source

theorem AleksandrovDifferentiability.secondOrderDifferentiableAEOn_of_fullMeasure_hilbertClmExpansionData {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [MeasurableSpace H] {μ : MeasureTheory.Measure H} {s G : Set H} {u : H → ℝ} (hs : MeasurableSet s) (hnull : μ (s \ G) = 0) (hG : ∀ ⦃x : H⦄, x ∈ s → x ∈ G → ∃ (ℓ : H →L[ℝ ] ℝ) (B : H →L[ℝ ] H), IsSymmetricOperator B ∧ HasSecondOrderExpansionAtCLM u x ℓ B) :

SecondOrderDifferentiableAEOn μ s u

In a real Hilbert space, full-measure CLM-gradient expansion data implies second-order differentiability almost everywhere on s.

source

theorem AleksandrovDifferentiability.measure_secondOrderBadSetOn_eq_zero_of_fullMeasure_hilbertClmExpansionData {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [MeasurableSpace H] {μ : MeasureTheory.Measure H} {s G : Set H} {u : H → ℝ} (hs : MeasurableSet s) (hnull : μ (s \ G) = 0) (hG : ∀ ⦃x : H⦄, x ∈ s → x ∈ G → ∃ (ℓ : H →L[ℝ ] ℝ) (B : H →L[ℝ ] H), IsSymmetricOperator B ∧ HasSecondOrderExpansionAtCLM u x ℓ B) :

μ (secondOrderBadSetOn s u) = 0

Null-bad-set version of secondOrderDifferentiableAEOn_of_fullMeasure_hilbertClmExpansionData.

source

theorem AleksandrovDifferentiability.restrict_measure_secondOrderBadSet_eq_zero_of_fullMeasure_hilbertClmExpansionData {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [MeasurableSpace H] {μ : MeasureTheory.Measure H} {s G : Set H} {u : H → ℝ} (hs : MeasurableSet s) (hnull : μ (s \ G) = 0) (hG : ∀ ⦃x : H⦄, x ∈ s → x ∈ G → ∃ (ℓ : H →L[ℝ ] ℝ) (B : H →L[ℝ ] H), IsSymmetricOperator B ∧ HasSecondOrderExpansionAtCLM u x ℓ B) :

(μ.restrict s) (secondOrderBadSet u) = 0

Restricted-measure null-bad-set version of secondOrderDifferentiableAEOn_of_fullMeasure_hilbertClmExpansionData.

source

theorem AleksandrovDifferentiability.secondOrderDifferentiableAEOn_of_countable_fullMeasure_hilbertClmExpansionData {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [MeasurableSpace H] {μ : MeasureTheory.Measure H} {s : Set H} {G : ℕ → Set H} {u : H → ℝ} (hs : MeasurableSet s) (hnull : ∀ (n : ℕ), μ (s \ G n) = 0) (hG : ∀ ⦃x : H⦄, x ∈ s → (∀ (n : ℕ), x ∈ G n) → ∃ (ℓ : H →L[ℝ ] ℝ) (B : H →L[ℝ ] H), IsSymmetricOperator B ∧ HasSecondOrderExpansionAtCLM u x ℓ B) :

SecondOrderDifferentiableAEOn μ s u

In a real Hilbert space, countably many full-measure good sets whose simultaneous validity gives CLM-gradient expansion data imply second-order differentiability almost everywhere on s.

source

theorem AleksandrovDifferentiability.measure_secondOrderBadSetOn_eq_zero_of_countable_fullMeasure_hilbertClmExpansionData {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [MeasurableSpace H] {μ : MeasureTheory.Measure H} {s : Set H} {G : ℕ → Set H} {u : H → ℝ} (hs : MeasurableSet s) (hnull : ∀ (n : ℕ), μ (s \ G n) = 0) (hG : ∀ ⦃x : H⦄, x ∈ s → (∀ (n : ℕ), x ∈ G n) → ∃ (ℓ : H →L[ℝ ] ℝ) (B : H →L[ℝ ] H), IsSymmetricOperator B ∧ HasSecondOrderExpansionAtCLM u x ℓ B) :

μ (secondOrderBadSetOn s u) = 0

Null-bad-set version of secondOrderDifferentiableAEOn_of_countable_fullMeasure_hilbertClmExpansionData.

source

theorem AleksandrovDifferentiability.restrict_measure_secondOrderBadSet_eq_zero_of_countable_fullMeasure_hilbertClmExpansionData {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [MeasurableSpace H] {μ : MeasureTheory.Measure H} {s : Set H} {G : ℕ → Set H} {u : H → ℝ} (hs : MeasurableSet s) (hnull : ∀ (n : ℕ), μ (s \ G n) = 0) (hG : ∀ ⦃x : H⦄, x ∈ s → (∀ (n : ℕ), x ∈ G n) → ∃ (ℓ : H →L[ℝ ] ℝ) (B : H →L[ℝ ] H), IsSymmetricOperator B ∧ HasSecondOrderExpansionAtCLM u x ℓ B) :

(μ.restrict s) (secondOrderBadSet u) = 0

Restricted-measure null-bad-set version of secondOrderDifferentiableAEOn_of_countable_fullMeasure_hilbertClmExpansionData.

source

theorem AleksandrovDifferentiability.secondOrderDifferentiableAEOn_of_fullMeasure_hilbertClmExpansionSet {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [MeasurableSpace H] {μ : MeasureTheory.Measure H} {s : Set H} {u : H → ℝ} {ℓ : H →L[ℝ ] ℝ} {B : H →L[ℝ ] H} (hs : MeasurableSet s) (hB : IsSymmetricOperator B) (hnull : μ (s \ secondOrderExpansionSetCLM u ℓ B) = 0) :

SecondOrderDifferentiableAEOn μ s u

If a fixed CLM expansion locus has full measure in s and the Hessian candidate is symmetric, then u is second-order differentiable almost everywhere on s.

source