LeanPool.SardMoreira.ChartEstimates

@[implicit_reducible]

instance Moreira2001.Chart.instMeasurableSpaceDom {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (ψ : Chart k α s) : MeasurableSpace ψ.Dom

Equations

• ψ.instMeasurableSpaceDom = borel ψ.Dom

instance Moreira2001.Chart.instBorelSpaceDom {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (ψ : Chart k α s) : BorelSpace ψ.Dom

theorem Moreira2001.Chart.eventually_contDiffAt_comp {E : Type u} {F : Type v} {G : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} {f : E × F → G} {ψ : Chart 1 α s} {x : E × ψ.Dom} (hx : x ∈ ψ.set) (hfk : ∀ᶠ (y : E × F) in nhdsWithin (↑ψ x) s, ContDiffMoreiraHolderAt k α f y) (hk : k ≠ 0) : ∀ᶠ (y : ψ.Dom) in nhds x.2, ContDiffAt ℝ 1 (fun (y : ψ.Dom) => f (↑ψ (x.1, y))) y

theorem Moreira2001.Chart.eventually_differentiableAt_comp {E : Type u} {F : Type v} {G : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} {f : E × F → G} {ψ : Chart 1 α s} {x : E × ψ.Dom} (hx : x ∈ ψ.set) (hfk : ∀ᶠ (y : E × F) in nhdsWithin (↑ψ x) s, ContDiffMoreiraHolderAt k α f y) (hk : k ≠ 0) : ∀ᶠ (y : ψ.Dom) in nhds x.2, DifferentiableAt ℝ (fun (y : ψ.Dom) => f (↑ψ (x.1, y))) y

theorem Moreira2001.Chart.fderiv₂_comp_eventuallyEq {E : Type u} {F : Type v} {G : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} {f : E × F → G} (ψ : Chart 1 α s) {x : E × ψ.Dom} (hx : x ∈ ψ.set) (hfk : ContDiffAt ℝ (↑k) f (↑ψ x)) (hk : k ≠ 0) : (fderiv ℝ fun (y : ψ.Dom) => f (↑ψ (x.1, y))) =ᶠ[nhds x.2] fun (y : ψ.Dom) => (fderiv ℝ f (↑ψ (x.1, y)) ∘SL ContinuousLinearMap.inr ℝ E F) ∘SL fderiv ℝ (fun (y : ψ.Dom) => (↑ψ (x.1, y)).2) y

theorem Moreira2001.Chart.step_aux {E : Type u} {F : Type v} {G : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} {f : E × F → G} (ψ : Chart 1 α s) {x : E × ψ.Dom} (hx : x ∈ ψ.set) (hfk : ContDiffAt ℝ (↑k) f (↑ψ x)) (hk : k ≠ 0) : (fderiv ℝ fun (y : ψ.Dom) => f (↑ψ (x.1, y))) =O[nhds x.2] fun (y : ψ.Dom) => fderiv ℝ f (↑ψ (x.1, y)) ∘SL ContinuousLinearMap.inr ℝ E F

theorem Moreira2001.Atlas.isBigO_main_aux {E : Type u} {F : Type v} {G : Type (max v w)} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} {f : E × F → G} {ψ : Chart 1 α s} {x : E × ψ.Dom} (hψ : ψ ∈ (main k α s).charts) (hx : x ∈ ψ.set) (hfk : ∀ᶠ (y : E × F) in nhdsWithin (↑ψ x) s, ContDiffMoreiraHolderAt k α f y) (hf₀ : f =ᶠ[nhdsWithin (↑ψ x) s] 0) : (fun (y : ψ.Dom) => f (↑ψ (x.1, y))) =O[nhds x.2] fun (y : ψ.Dom) => ‖y - x.2‖ ^ (↑k + ↑α)

theorem Moreira2001.Atlas.isBigO_main_inr {E : Type u} {F : Type v} {G : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} {f : E × F → G} {ψ : Chart 1 α s} {x : E × ψ.Dom} (hψ : ψ ∈ (main k α s).charts) (hx : x ∈ ψ.set) (hfk : ∀ᶠ (y : E × F) in nhdsWithin (↑ψ x) s, ContDiffMoreiraHolderAt k α f y) (hf₀ : f =ᶠ[nhdsWithin (↑ψ x) s] 0) : (fun (y : ψ.Dom) => f (↑ψ (x.1, y))) =O[nhds x.2] fun (y : ψ.Dom) => ‖y - x.2‖ ^ (↑k + ↑α)

theorem Moreira2001.Atlas.isBigO_main_sub_of_fderiv_zero_right {E : Type u} {F : Type v} {G : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} {f : E × F → G} {ψ : Chart 1 α s} {x : E × ψ.Dom} (hψ : ψ ∈ (main k α s).charts) (hx : x ∈ ψ.set) (hfk : ∀ᶠ (y : E × F) in nhdsWithin (↑ψ x) s, ContDiffMoreiraHolderAt (k + 1) α f y) (hf₀ : (fun (x : E × F) => fderiv ℝ f x ∘SL ContinuousLinearMap.inr ℝ E F) =ᶠ[nhdsWithin (↑ψ x) s] 0) : (fun (y : ψ.Dom) => f (↑ψ (x.1, y)) - f (↑ψ x)) =O[nhds x.2] fun (y : ψ.Dom) => ‖y - x.2‖ ^ (↑k + 1 + ↑α)

theorem Moreira2001.Atlas.isLittleO_main_sub_of_fderiv_zero_right {E : Type u} {F : Type v} {G : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} {f : E × F → G} {ψ : Chart 1 α s} {x : E × ψ.Dom} (hψ : ψ ∈ (main k α s).charts) (hx : x ∈ ψ.set) (hfk : ∀ᶠ (y : E × F) in nhdsWithin (↑ψ x) s, ContDiffMoreiraHolderAt (k + 1) α f y) (hf₀ : (fun (x : E × F) => fderiv ℝ f x ∘SL ContinuousLinearMap.inr ℝ E F) =ᶠ[nhdsWithin (↑ψ x) s] 0) (hdensity : Filter.Tendsto (fun (r : ℝ) => (MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ ψ.Dom)) ({y : ψ.Dom | (x.1, y) ∈ closure ψ.set} ∩ Metric.closedBall x.2 r) / (MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ ψ.Dom)) (Metric.closedBall x.2 r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)) : (fun (y : ψ.Dom) => f (↑ψ (x.1, y)) - f (↑ψ x)) =o[nhds x.2] fun (y : ψ.Dom) => ‖y - x.2‖ ^ (↑k + 1 + ↑α)