LeanPool.SardMoreira.LocalEstimates

theorem UniformSpace.Completion.hasFDerivAt_coe {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {a : E} : HasFDerivAt coe' toComplL a

theorem openSegment_subset_ball_left {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x y : E} (h : x ≠ y) : openSegment ℝ x y ⊆ Metric.ball x ‖y - x‖

theorem dist_le_mul_volume_of_norm_lineDeriv_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {a b : E} {C : ℝ} (hfc : ContinuousOn f (segment ℝ a b)) (hfd : ∀ t ∈ Set.Ioo 0 1, LineDifferentiableAt ℝ f ((AffineMap.lineMap a b) t) (b - a)) (hf' : ∀ᵐ (t : ℝ), t ∈ Set.Ioo 0 1 → ‖lineDeriv ℝ f ((AffineMap.lineMap a b) t) (b - a)‖ ≤ C) : ‖f b - f a‖ ≤ C * MeasureTheory.volume.real {t : ℝ | t ∈ Set.Ioo 0 1 ∧ lineDeriv ℝ f ((AffineMap.lineMap a b) t) (b - a) ≠ 0}

theorem dist_le_mul_volume_of_norm_fderiv_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {a b : E} {C : ℝ} {s : Set E} (hs : IsOpen s) (hf : DiffContOnCl ℝ f s) (hab : openSegment ℝ a b ⊆ s) (hC : ∀ x ∈ s, ‖fderiv ℝ f x‖ ≤ C) : ‖f b - f a‖ ≤ C * ‖b - a‖ * MeasureTheory.volume.real {t : ℝ | t ∈ Set.Ioo 0 1 ∧ fderiv ℝ f ((AffineMap.lineMap a b) t) ≠ 0}

theorem sub_isBigO_norm_rpow_add_one_of_fderiv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {a : E} {r : ℝ} (hr : 0 ≤ r) (hdf : ∀ᶠ (x : E) in nhds a, DifferentiableAt ℝ f x) (hderiv : fderiv ℝ f =O[nhds a] fun (x : E) => ‖x - a‖ ^ r) : (fun (x : E) => f x - f a) =O[nhds a] fun (x : E) => ‖x - a‖ ^ (r + 1)

theorem isBigO_norm_rpow_add_one_of_fderiv_of_apply_eq_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {a : E} {r : ℝ} (hr : 0 ≤ r) (hdf : ∀ᶠ (x : E) in nhds a, DifferentiableAt ℝ f x) (hderiv : fderiv ℝ f =O[nhds a] fun (x : E) => ‖x - a‖ ^ r) (hf₀ : f a = 0) : f =O[nhds a] fun (x : E) => ‖x - a‖ ^ (r + 1)

theorem sub_isLittleO_norm_rpow_add_one_of_fderiv_of_density_point {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {f : E → F} {a : E} {r : ℝ} {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {s : Set E} (hr : 0 ≤ r) (hdf : ∀ᶠ (x : E) in nhds a, DifferentiableAt ℝ f x) (hderiv : fderiv ℝ f =O[nhds a] fun (x : E) => ‖x - a‖ ^ r) (hs : fderiv ℝ f =ᶠ[nhdsWithin a s] 0) (hmeas : Filter.Tendsto (fun (r : ℝ) => μ (s ∩ Metric.closedBall a r) / μ (Metric.closedBall a r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)) : (fun (x : E) => f x - f a) =o[nhds a] fun (x : E) => ‖x - a‖ ^ (r + 1)

theorem isLittleO_norm_rpow_add_one_of_fderiv_of_density_point_of_apply_eq_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {f : E → F} {a : E} {r : ℝ} {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {s : Set E} (hr : 0 ≤ r) (hdf : ∀ᶠ (x : E) in nhds a, DifferentiableAt ℝ f x) (hderiv : fderiv ℝ f =O[nhds a] fun (x : E) => ‖x - a‖ ^ r) (hs : ∀ᶠ (x : E) in nhdsWithin a s, fderiv ℝ f x = 0) (hmeas : Filter.Tendsto (fun (r : ℝ) => μ (s ∩ Metric.closedBall a r) / μ (Metric.closedBall a r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)) (hf₀ : f a = 0) : f =o[nhds a] fun (x : E) => ‖x - a‖ ^ (r + 1)