LeanPool.SardMoreira.MainTheorem

noncomputable def ContinuousLinearMap.finrank {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (f : M →L[R] N) : ℕ

The dimension of the range of a continuous linear map.

Equations

• f.finrank = Module.finrank R ↥(↑f).range

theorem ContinuousLinearMap.finrank_comp_eq_left_of_surjective {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [AddCommMonoid P] [Module R P] [TopologicalSpace P] (g : N →L[R] P) {f : M →L[R] N} (hf : Function.Surjective ⇑f) : (g ∘SL f).finrank = g.finrank

theorem ContinuousLinearMap.finrank_comp_eq_right_of_injective {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [AddCommMonoid P] [Module R P] [TopologicalSpace P] {g : N →L[R] P} (hg : Function.Injective ⇑g) (f : M →L[R] N) : (g ∘SL f).finrank = f.finrank

@[simp]

theorem ContinuousLinearEquiv.finrank_comp_left {R : Type u_1} {M : Type u_2} {N : Type u_3} {N' : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [AddCommMonoid N'] [Module R N'] [TopologicalSpace N'] (e : N ≃L[R] N') (f : M →L[R] N) : (↑e ∘SL f).finrank = f.finrank

@[simp]

theorem ContinuousLinearEquiv.finrank_comp_right {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] [AddCommMonoid M'] [Module R M'] [TopologicalSpace M'] (f : M →L[R] N) (e : M' ≃L[R] M) : (f ∘SL ↑e).finrank = f.finrank

theorem LipschitzWith.hausdorffMeasure_image_null {X : Type u_1} {Y : Type u_2} [EMetricSpace X] [EMetricSpace Y] [MeasurableSpace X] [BorelSpace X] [MeasurableSpace Y] [BorelSpace Y] {K : NNReal} {f : X → Y} (h : LipschitzWith K f) {d : ℝ} (hd : 0 ≤ d) {s : Set X} (hs : (MeasureTheory.Measure.hausdorffMeasure d) s = 0) : (MeasureTheory.Measure.hausdorffMeasure d) (f '' s) = 0

noncomputable def sardMoreiraBound (n k : ℕ) (α : ↑unitInterval) (p : ℕ) : NNReal

Moreira's upper estimate on the Hausdorff dimension of the image of the set of points $x$ such that fderiv ℝ f x has rank at most p < min n m, provided that f is a $$C^{k+(\alpha)}$$-map from an n-dimensional space to an m-dimensional space.

Note that the estimate does not depend on m.

Equations

• sardMoreiraBound n k α p = ⟨↑p + ↑(n - p) / (↑k + ↑α), ⋯⟩

theorem mul_sardMoreiraBound {n k p : ℕ} (hk : k ≠ 0) (hpn : p ≤ n) (α : ↑unitInterval) : (↑k + ↑α) * ↑(sardMoreiraBound n k α p) = (↑k + ↑α) * ↑p + (↑n - ↑p)

theorem monotone_sardMoreiraBound (n : ℕ) {k : ℕ} (hk : k ≠ 0) (α : ↑unitInterval) : Monotone (sardMoreiraBound n k α)

theorem sardMoreiraBound_le_sardMoreiraBound {m n k l p q : ℕ} (hl : l ≠ 0) (hmn : m ≤ n) (hlk : l ≤ k) (hpq : p ≤ q) (α : ↑unitInterval) : sardMoreiraBound m k α p ≤ sardMoreiraBound n l α q

theorem Moreira2001.hausdorffMeasure_image_le_mul_aux {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {X : Type u_4} [MetricSpace X] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [MeasurableSpace X] [BorelSpace X] {f : E × F → X} {s : Set (E × F)} {n : ℕ} (hk : k ≠ 0) (hn : Module.finrank ℝ E + Module.finrank ℝ F ≤ n) {cE cF : NNReal} (hcE : ∀ x ∈ s, ∀ᶠ (y : (E × F) × E × F) in nhds (x, x), y.1.2 = y.2.2 → dist (f y.1) (f y.2) ≤ ↑cE * dist y.1 y.2) (hcF : ∀ x ∈ s, ∀ᶠ (y : F) in nhds x.2, dist (f (x.1, y)) (f x) ≤ ↑cF * dist y x.2 ^ (↑k + ↑α)) : (MeasureTheory.Measure.hausdorffMeasure ↑(sardMoreiraBound n k α (Module.finrank ℝ E))) (f '' s) ≤ (2 * (↑cE + ↑cF)) ^ ↑(sardMoreiraBound n k α (Module.finrank ℝ E)) / ((MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ E)) (Metric.ball 0 1) * (MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ F)) (Metric.ball 0 1)) * ((MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ E)).prod (MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ F))) s

noncomputable def Moreira2001.boundCoeff (E : Type u_1) (F : Type u_2) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (n k : ℕ) (α : ↑unitInterval) : ENNReal

The coefficient appearing in Moreira's Hausdorff-measure estimate.

Equations

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

theorem Moreira2001.hausdorffMeasure_image_le_mul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {X : Type u_4} [MetricSpace X] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [MeasurableSpace X] [BorelSpace X] {f : E × F → X} {s : Set (E × F)} {n : ℕ} (hk : k ≠ 0) (hn : Module.finrank ℝ E + Module.finrank ℝ F ≤ n) {cE cF : NNReal} (hcE₀ : cE ≠ 0) (hcF₀ : cF ≠ 0) (hcE : ∀ x ∈ s, ∀ᶠ (y : (E × F) × E × F) in nhds (x, x), y.1.2 = y.2.2 → dist (f y.1) (f y.2) ≤ ↑cE * dist y.1 y.2) (hcF : ∀ x ∈ s, ∀ᶠ (y : F) in nhds x.2, dist (f (x.1, y)) (f x) ≤ ↑cF * dist y x.2 ^ (↑k + ↑α)) : (MeasureTheory.Measure.hausdorffMeasure ↑(sardMoreiraBound n k α (Module.finrank ℝ E))) (f '' s) ≤ boundCoeff E F n k α * ↑cE ^ Module.finrank ℝ E * ↑cF ^ ((↑n - ↑(Module.finrank ℝ E)) / (↑k + ↑α)) * ((MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ E)).prod (MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ F))) s

theorem Moreira2001.hausdorffMeasure_image_null_of_isBigO {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {X : Type u_4} [MetricSpace X] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace F] [BorelSpace F] [MeasurableSpace X] [BorelSpace X] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {f : E × F → X} {s : Set (E × F)} {n : ℕ} {cE : NNReal} (hk : k ≠ 0) (hn : Module.finrank ℝ E + Module.finrank ℝ F ≤ n) (hcE : ∀ x ∈ s, ∀ᶠ (y : (E × F) × E × F) in nhds (x, x), y.1.2 = y.2.2 → dist (f y.1) (f y.2) ≤ ↑cE * dist y.1 y.2) (h_isBigO : ∀ x ∈ s, (fun (y : F) => dist (f (x.1, y)) (f x)) =O[nhds x.2] fun (y : F) => ‖y - x.2‖ ^ (↑k + ↑α)) (hs : ((MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ E)).prod (MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ F))) s = 0) : (MeasureTheory.Measure.hausdorffMeasure ↑(sardMoreiraBound n k α (Module.finrank ℝ E))) (f '' s) = 0

theorem Moreira2001.hausdorffMeasure_image_null_of_isLittleO {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {X : Type u_4} [MetricSpace X] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace F] [BorelSpace F] [MeasurableSpace X] [BorelSpace X] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {f : E × F → X} {s : Set (E × F)} {n : ℕ} {cE : NNReal} (hk : k ≠ 0) (hnp : Module.finrank ℝ E < n) (hn : Module.finrank ℝ E + Module.finrank ℝ F ≤ n) (hcE : ∀ x ∈ s, ∀ᶠ (y : (E × F) × E × F) in nhds (x, x), y.1.2 = y.2.2 → dist (f y.1) (f y.2) ≤ ↑cE * dist y.1 y.2) (h_isLittleO : ∀ x ∈ s, (fun (y : F) => dist (f (x.1, y)) (f x)) =o[nhds x.2] fun (y : F) => ‖y - x.2‖ ^ (↑k + ↑α)) : (MeasureTheory.Measure.hausdorffMeasure ↑(sardMoreiraBound n k α (Module.finrank ℝ E))) (f '' s) = 0

theorem Moreira2001.hausdorffMeasure_image_piProd_fst_null_of_isBigO_isLittleO {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {k : ℕ} {α : ↑unitInterval} [MeasurableSpace E] [BorelSpace E] [MeasurableSpace F] [BorelSpace F] [MeasurableSpace G] [BorelSpace G] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {f : E × F → G} {s : Set (E × F)} {n : ℕ} (hk : k ≠ 0) (hnp : Module.finrank ℝ E < n) (hn : Module.finrank ℝ E + Module.finrank ℝ F ≤ n) (h_contDiff : ∀ x ∈ s, ContDiffAt ℝ 1 f x) (h_isBigO : ∀ x ∈ s, (fun (y : F) => f (x.1, y) - f x) =O[nhds x.2] fun (y : F) => ‖y - x.2‖ ^ (↑k + ↑α)) (h_isLittleO : ∀ᵐ (x : E × F) ∂(MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ E)).prod (MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ F)), x ∈ s → (fun (y : F) => f (x.1, y) - f x) =o[nhds x.2] fun (y : F) => ‖y - x.2‖ ^ (↑k + ↑α)) : (MeasureTheory.Measure.hausdorffMeasure ↑(sardMoreiraBound n k α (Module.finrank ℝ E))) (Function.prod Prod.fst f '' s) = 0

theorem Moreira2001.hausdorffMeasure_image_piProd_fst_null_of_fderiv_comp_inr_zero {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {k : ℕ} {α : ↑unitInterval} [MeasurableSpace E] [BorelSpace E] [MeasurableSpace G] [BorelSpace G] [Nontrivial F] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {f : E × F → G} {s : Set (E × F)} (hf : ∀ x ∈ s, ContDiffMoreiraHolderAt k α f x) (hk : k ≠ 0) (hs : ∀ x ∈ s, fderiv ℝ f x ∘SL ContinuousLinearMap.inr ℝ E F = 0) : (MeasureTheory.Measure.hausdorffMeasure ↑(sardMoreiraBound (Module.finrank ℝ E + Module.finrank ℝ F) k α (Module.finrank ℝ E))) (Function.prod Prod.fst f '' s) = 0

theorem Moreira2001.hausdorffMeasure_image_piProd_fst_null_of_finrank_eq {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {k : ℕ} {α : ↑unitInterval} [MeasurableSpace E] [BorelSpace E] [MeasurableSpace G] [BorelSpace G] [Nontrivial F] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {f : E × F → G} {s : Set (E × F)} (hf : ∀ x ∈ s, ContDiffMoreiraHolderAt k α f x) (hk : k ≠ 0) (hs : ∀ x ∈ s, Module.finrank ℝ ↥(↑(fderiv ℝ (Function.prod Prod.fst f) x)).range = Module.finrank ℝ E) : (MeasureTheory.Measure.hausdorffMeasure ↑(sardMoreiraBound (Module.finrank ℝ E + Module.finrank ℝ F) k α (Module.finrank ℝ E))) (Function.prod Prod.fst f '' s) = 0

theorem Moreira2001.hausdorffMeasure_image_nhdsWithin_null_of_finrank_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k p : ℕ} {α : ↑unitInterval} [CompleteSpace F] [MeasurableSpace F] [BorelSpace F] (hp_dom : p < Module.finrank ℝ E) (hk : k ≠ 0) {f : E → F} {s : Set E} (hf : ∀ x ∈ s, ContDiffMoreiraHolderAt k α f x) (hs : ∀ x ∈ s, (fderiv ℝ f x).finrank = p) {a : E} (ha : a ∈ s) : ∃ t ∈ nhdsWithin a s, (MeasureTheory.Measure.hausdorffMeasure ↑(sardMoreiraBound (Module.finrank ℝ E) k α p)) (f '' t) = 0

theorem Moreira2001.hausdorffMeasure_image_null_of_finrank_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k p : ℕ} {α : ↑unitInterval} [MeasurableSpace F] [BorelSpace F] [CompleteSpace F] (hp_dom : p < Module.finrank ℝ E) (hk : k ≠ 0) {f : E → F} {s : Set E} (hf : ∀ x ∈ s, ContDiffMoreiraHolderAt k α f x) (hs : ∀ x ∈ s, Module.finrank ℝ ↥(↑(fderiv ℝ f x)).range = p) : (MeasureTheory.Measure.hausdorffMeasure ↑(sardMoreiraBound (Module.finrank ℝ E) k α p)) (f '' s) = 0

theorem hausdorffMeasure_sardMoreiraBound_image_null_of_finrank_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k p : ℕ} {α : ↑unitInterval} [MeasurableSpace F] [BorelSpace F] (hp_dom : p < Module.finrank ℝ E) (hk : k ≠ 0) {f : E → F} {s : Set E} (hf : ∀ x ∈ s, ContDiffMoreiraHolderAt k α f x) (hs : ∀ x ∈ s, Module.finrank ℝ ↥(↑(fderiv ℝ f x)).range ≤ p) : (MeasureTheory.Measure.hausdorffMeasure ↑(sardMoreiraBound (Module.finrank ℝ E) k α p)) (f '' s) = 0

theorem dimH_image_le_sardMoreiraBound_of_finrank_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k p : ℕ} {α : ↑unitInterval} (hp_dom : p < Module.finrank ℝ E) (hk : k ≠ 0) {f : E → F} {s : Set E} (hf : ∀ x ∈ s, ContDiffMoreiraHolderAt k α f x) (hs : ∀ x ∈ s, Module.finrank ℝ ↥(↑(fderiv ℝ f x)).range ≤ p) : dimH (f '' s) ≤ ↑(sardMoreiraBound (Module.finrank ℝ E) k α p)