[GOAL]
G : Type uG
E' : Type uE'
inst✝⁶ : NormedAddCommGroup E'
g : G → E'
inst✝⁵ : MeasurableSpace G
μ : Measure G
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : HasContDiffBump G
inst✝ : CompleteSpace E'
φ : ContDiffBump 0
x₀✝ x₀ : G
hg : ∀ (x : G), x ∈ ball x₀ φ.rOut → g x = g x₀
⊢ ↑φ ⋆[lsmul ℝ ℝ, x₀] g = integral μ ↑φ • g x₀
[PROOFSTEP]
simp_rw [convolution_eq_right' _ φ.support_eq.subset hg, lsmul_apply, integral_smul_const]
[GOAL]
G : Type uG
E' : Type uE'
inst✝¹⁰ : NormedAddCommGroup E'
g : G → E'
inst✝⁹ : MeasurableSpace G
μ : Measure G
inst✝⁸ : NormedSpace ℝ E'
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : HasContDiffBump G
inst✝⁴ : CompleteSpace E'
φ : ContDiffBump 0
x₀✝ : G
inst✝³ : BorelSpace G
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : FiniteDimensional ℝ G
x₀ : G
hg : ∀ (x : G), x ∈ ball x₀ φ.rOut → g x = g x₀
⊢ ContDiffBump.normed φ μ ⋆[lsmul ℝ ℝ, x₀] g = g x₀
[PROOFSTEP]
rw [convolution_eq_right' _ φ.support_normed_eq.subset hg]
[GOAL]
G : Type uG
E' : Type uE'
inst✝¹⁰ : NormedAddCommGroup E'
g : G → E'
inst✝⁹ : MeasurableSpace G
μ : Measure G
inst✝⁸ : NormedSpace ℝ E'
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : HasContDiffBump G
inst✝⁴ : CompleteSpace E'
φ : ContDiffBump 0
x₀✝ : G
inst✝³ : BorelSpace G
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : FiniteDimensional ℝ G
x₀ : G
hg : ∀ (x : G), x ∈ ball x₀ φ.rOut → g x = g x₀
⊢ ∫ (t : G), ↑(↑(lsmul ℝ ℝ) (ContDiffBump.normed φ μ t)) (g x₀) ∂μ = g x₀
[PROOFSTEP]
exact integral_normed_smul φ μ (g x₀)
[GOAL]
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ : ContDiffBump 0
x₀✝ : G
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : IsOpenPosMeasure μ
inst✝¹ : FiniteDimensional ℝ G
inst✝ : IsAddLeftInvariant μ
x₀ : G
ε : ℝ
hmg : AEStronglyMeasurable g μ
hg : ∀ (x : G), x ∈ ball x₀ φ.rOut → dist (g x) (g x₀) ≤ ε
⊢ 0 ≤ ε
[PROOFSTEP]
simp_rw [← dist_self (g x₀), hg x₀ (mem_ball_self φ.rOut_pos)]
[GOAL]
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ✝ : ContDiffBump 0
x₀ : G
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : IsOpenPosMeasure μ
inst✝¹ : FiniteDimensional ℝ G
inst✝ : IsAddLeftInvariant μ
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g
⊢ ∀ᵐ (x₀ : G) ∂μ, Tendsto (fun i => ContDiffBump.normed (φ i) μ ⋆[lsmul ℝ ℝ, x₀] g) l (𝓝 (g x₀))
[PROOFSTEP]
have : IsAddHaarMeasure μ :=
  ⟨⟩
    -- By Lebesgue differentiation theorem, the average of `g` on a small ball converges
      -- almost everywhere to the value of `g` as the radius shrinks to zero.
      -- We will see that this set of points satisfies the desired conclusion.
[GOAL]
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ✝ : ContDiffBump 0
x₀ : G
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : IsOpenPosMeasure μ
inst✝¹ : FiniteDimensional ℝ G
inst✝ : IsAddLeftInvariant μ
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g
this : IsAddHaarMeasure μ
⊢ ∀ᵐ (x₀ : G) ∂μ, Tendsto (fun i => ContDiffBump.normed (φ i) μ ⋆[lsmul ℝ ℝ, x₀] g) l (𝓝 (g x₀))
[PROOFSTEP]
filter_upwards [(Besicovitch.vitaliFamily μ).ae_tendsto_average_norm_sub hg] with x₀ h₀
[GOAL]
case h
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ✝ : ContDiffBump 0
x₀✝ : G
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : IsOpenPosMeasure μ
inst✝¹ : FiniteDimensional ℝ G
inst✝ : IsAddLeftInvariant μ
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g
this : IsAddHaarMeasure μ
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
⊢ Tendsto (fun i => ContDiffBump.normed (φ i) μ ⋆[lsmul ℝ ℝ, x₀] g) l (𝓝 (g x₀))
[PROOFSTEP]
simp only [convolution_eq_swap, lsmul_apply]
[GOAL]
case h
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ✝ : ContDiffBump 0
x₀✝ : G
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : IsOpenPosMeasure μ
inst✝¹ : FiniteDimensional ℝ G
inst✝ : IsAddLeftInvariant μ
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g
this : IsAddHaarMeasure μ
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
⊢ Tendsto (fun i => ∫ (t : G), ContDiffBump.normed (φ i) μ (x₀ - t) • g t ∂μ) l (𝓝 (g x₀))
[PROOFSTEP]
have hφ' : Tendsto (fun i ↦ (φ i).rOut) l (𝓝[>] 0) :=
  tendsto_nhdsWithin_iff.2 ⟨hφ, eventually_of_forall (fun i ↦ (φ i).rOut_pos)⟩
[GOAL]
case h
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ✝ : ContDiffBump 0
x₀✝ : G
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : IsOpenPosMeasure μ
inst✝¹ : FiniteDimensional ℝ G
inst✝ : IsAddLeftInvariant μ
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g
this : IsAddHaarMeasure μ
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[Ioi 0] 0)
⊢ Tendsto (fun i => ∫ (t : G), ContDiffBump.normed (φ i) μ (x₀ - t) • g t ∂μ) l (𝓝 (g x₀))
[PROOFSTEP]
have := (h₀.comp (Besicovitch.tendsto_filterAt μ x₀)).comp hφ'
[GOAL]
case h
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ✝ : ContDiffBump 0
x₀✝ : G
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : IsOpenPosMeasure μ
inst✝¹ : FiniteDimensional ℝ G
inst✝ : IsAddLeftInvariant μ
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g
this✝ : IsAddHaarMeasure μ
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[Ioi 0] 0)
this : Tendsto (((fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun r => closedBall x₀ r) ∘ fun i => (φ i).rOut) l (𝓝 0)
⊢ Tendsto (fun i => ∫ (t : G), ContDiffBump.normed (φ i) μ (x₀ - t) • g t ∂μ) l (𝓝 (g x₀))
[PROOFSTEP]
simp only [Function.comp] at this
[GOAL]
case h
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ✝ : ContDiffBump 0
x₀✝ : G
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : IsOpenPosMeasure μ
inst✝¹ : FiniteDimensional ℝ G
inst✝ : IsAddLeftInvariant μ
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g
this✝ : IsAddHaarMeasure μ
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[Ioi 0] 0)
this : Tendsto (fun x => ⨍ (y : G) in closedBall x₀ (φ x).rOut, ‖g y - g x₀‖ ∂μ) l (𝓝 0)
⊢ Tendsto (fun i => ∫ (t : G), ContDiffBump.normed (φ i) μ (x₀ - t) • g t ∂μ) l (𝓝 (g x₀))
[PROOFSTEP]
apply tendsto_integral_smul_of_tendsto_average_norm_sub (K ^ (FiniteDimensional.finrank ℝ G)) this
[GOAL]
case h.f_int
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ✝ : ContDiffBump 0
x₀✝ : G
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : IsOpenPosMeasure μ
inst✝¹ : FiniteDimensional ℝ G
inst✝ : IsAddLeftInvariant μ
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g
this✝ : IsAddHaarMeasure μ
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[Ioi 0] 0)
this : Tendsto (fun x => ⨍ (y : G) in closedBall x₀ (φ x).rOut, ‖g y - g x₀‖ ∂μ) l (𝓝 0)
⊢ ∀ᶠ (i : ι) in l, IntegrableOn (fun y => g y) (closedBall x₀ (φ i).rOut)
[PROOFSTEP]
apply eventually_of_forall (fun i ↦ ?_)
[GOAL]
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ✝ : ContDiffBump 0
x₀✝ : G
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : IsOpenPosMeasure μ
inst✝¹ : FiniteDimensional ℝ G
inst✝ : IsAddLeftInvariant μ
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g
this✝ : IsAddHaarMeasure μ
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[Ioi 0] 0)
this : Tendsto (fun x => ⨍ (y : G) in closedBall x₀ (φ x).rOut, ‖g y - g x₀‖ ∂μ) l (𝓝 0)
i : ι
⊢ IntegrableOn (fun y => g y) (closedBall x₀ (φ i).rOut)
[PROOFSTEP]
apply hg.integrableOn_isCompact
[GOAL]
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ✝ : ContDiffBump 0
x₀✝ : G
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : IsOpenPosMeasure μ
inst✝¹ : FiniteDimensional ℝ G
inst✝ : IsAddLeftInvariant μ
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g
this✝ : IsAddHaarMeasure μ
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[Ioi 0] 0)
this : Tendsto (fun x => ⨍ (y : G) in closedBall x₀ (φ x).rOut, ‖g y - g x₀‖ ∂μ) l (𝓝 0)
i : ι
⊢ IsCompact (closedBall x₀ (φ i).rOut)
[PROOFSTEP]
exact isCompact_closedBall _ _
[GOAL]
case h.hg
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ✝ : ContDiffBump 0
x₀✝ : G
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : IsOpenPosMeasure μ
inst✝¹ : FiniteDimensional ℝ G
inst✝ : IsAddLeftInvariant μ
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g
this✝ : IsAddHaarMeasure μ
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[Ioi 0] 0)
this : Tendsto (fun x => ⨍ (y : G) in closedBall x₀ (φ x).rOut, ‖g y - g x₀‖ ∂μ) l (𝓝 0)
⊢ Tendsto (fun i => ∫ (y : G), ContDiffBump.normed (φ i) μ (x₀ - y) ∂μ) l (𝓝 1)
[PROOFSTEP]
apply tendsto_const_nhds.congr (fun i ↦ ?_)
[GOAL]
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ✝ : ContDiffBump 0
x₀✝ : G
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : IsOpenPosMeasure μ
inst✝¹ : FiniteDimensional ℝ G
inst✝ : IsAddLeftInvariant μ
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g
this✝ : IsAddHaarMeasure μ
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[Ioi 0] 0)
this : Tendsto (fun x => ⨍ (y : G) in closedBall x₀ (φ x).rOut, ‖g y - g x₀‖ ∂μ) l (𝓝 0)
i : ι
⊢ 1 = ∫ (y : G), ContDiffBump.normed (φ i) μ (x₀ - y) ∂μ
[PROOFSTEP]
rw [← integral_neg_eq_self]
[GOAL]
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ✝ : ContDiffBump 0
x₀✝ : G
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : IsOpenPosMeasure μ
inst✝¹ : FiniteDimensional ℝ G
inst✝ : IsAddLeftInvariant μ
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g
this✝ : IsAddHaarMeasure μ
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[Ioi 0] 0)
this : Tendsto (fun x => ⨍ (y : G) in closedBall x₀ (φ x).rOut, ‖g y - g x₀‖ ∂μ) l (𝓝 0)
i : ι
⊢ 1 = ∫ (x : G), ContDiffBump.normed (φ i) μ (x₀ - -x) ∂μ
[PROOFSTEP]
simp only [sub_neg_eq_add, integral_add_left_eq_self, integral_normed]
[GOAL]
case h.g_supp
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ✝ : ContDiffBump 0
x₀✝ : G
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : IsOpenPosMeasure μ
inst✝¹ : FiniteDimensional ℝ G
inst✝ : IsAddLeftInvariant μ
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g
this✝ : IsAddHaarMeasure μ
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[Ioi 0] 0)
this : Tendsto (fun x => ⨍ (y : G) in closedBall x₀ (φ x).rOut, ‖g y - g x₀‖ ∂μ) l (𝓝 0)
⊢ ∀ᶠ (i : ι) in l, (support fun y => ContDiffBump.normed (φ i) μ (x₀ - y)) ⊆ closedBall x₀ (φ i).rOut
[PROOFSTEP]
apply eventually_of_forall (fun i ↦ ?_)
[GOAL]
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ✝ : ContDiffBump 0
x₀✝ : G
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : IsOpenPosMeasure μ
inst✝¹ : FiniteDimensional ℝ G
inst✝ : IsAddLeftInvariant μ
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g
this✝ : IsAddHaarMeasure μ
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[Ioi 0] 0)
this : Tendsto (fun x => ⨍ (y : G) in closedBall x₀ (φ x).rOut, ‖g y - g x₀‖ ∂μ) l (𝓝 0)
i : ι
⊢ (support fun y => ContDiffBump.normed (φ i) μ (x₀ - y)) ⊆ closedBall x₀ (φ i).rOut
[PROOFSTEP]
change support ((ContDiffBump.normed (φ i) μ) ∘ (fun y ↦ x₀ - y)) ⊆ closedBall x₀ (φ i).rOut
[GOAL]
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ✝ : ContDiffBump 0
x₀✝ : G
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : IsOpenPosMeasure μ
inst✝¹ : FiniteDimensional ℝ G
inst✝ : IsAddLeftInvariant μ
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g
this✝ : IsAddHaarMeasure μ
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[Ioi 0] 0)
this : Tendsto (fun x => ⨍ (y : G) in closedBall x₀ (φ x).rOut, ‖g y - g x₀‖ ∂μ) l (𝓝 0)
i : ι
⊢ support (ContDiffBump.normed (φ i) μ ∘ fun y => x₀ - y) ⊆ closedBall x₀ (φ i).rOut
[PROOFSTEP]
simp only [support_comp_eq_preimage, support_normed_eq]
[GOAL]
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ✝ : ContDiffBump 0
x₀✝ : G
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : IsOpenPosMeasure μ
inst✝¹ : FiniteDimensional ℝ G
inst✝ : IsAddLeftInvariant μ
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g
this✝ : IsAddHaarMeasure μ
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[Ioi 0] 0)
this : Tendsto (fun x => ⨍ (y : G) in closedBall x₀ (φ x).rOut, ‖g y - g x₀‖ ∂μ) l (𝓝 0)
i : ι
⊢ (fun y => x₀ - y) ⁻¹' ball 0 (φ i).rOut ⊆ closedBall x₀ (φ i).rOut
[PROOFSTEP]
intro x hx
[GOAL]
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ✝ : ContDiffBump 0
x₀✝ : G
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : IsOpenPosMeasure μ
inst✝¹ : FiniteDimensional ℝ G
inst✝ : IsAddLeftInvariant μ
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g
this✝ : IsAddHaarMeasure μ
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[Ioi 0] 0)
this : Tendsto (fun x => ⨍ (y : G) in closedBall x₀ (φ x).rOut, ‖g y - g x₀‖ ∂μ) l (𝓝 0)
i : ι
x : G
hx : x ∈ (fun y => x₀ - y) ⁻¹' ball 0 (φ i).rOut
⊢ x ∈ closedBall x₀ (φ i).rOut
[PROOFSTEP]
simp only [mem_preimage, mem_ball, dist_zero_right] at hx
[GOAL]
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ✝ : ContDiffBump 0
x₀✝ : G
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : IsOpenPosMeasure μ
inst✝¹ : FiniteDimensional ℝ G
inst✝ : IsAddLeftInvariant μ
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g
this✝ : IsAddHaarMeasure μ
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[Ioi 0] 0)
this : Tendsto (fun x => ⨍ (y : G) in closedBall x₀ (φ x).rOut, ‖g y - g x₀‖ ∂μ) l (𝓝 0)
i : ι
x : G
hx : ‖x₀ - x‖ < (φ i).rOut
⊢ x ∈ closedBall x₀ (φ i).rOut
[PROOFSTEP]
simpa [dist_eq_norm_sub'] using hx.le
[GOAL]
case h.g_bound
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ✝ : ContDiffBump 0
x₀✝ : G
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : IsOpenPosMeasure μ
inst✝¹ : FiniteDimensional ℝ G
inst✝ : IsAddLeftInvariant μ
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g
this✝ : IsAddHaarMeasure μ
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[Ioi 0] 0)
this : Tendsto (fun x => ⨍ (y : G) in closedBall x₀ (φ x).rOut, ‖g y - g x₀‖ ∂μ) l (𝓝 0)
⊢ ∀ᶠ (i : ι) in l,
    ∀ (x : G),
      |ContDiffBump.normed (φ i) μ (x₀ - x)| ≤
        K ^ FiniteDimensional.finrank ℝ G / ENNReal.toReal (↑↑μ (closedBall x₀ (φ i).rOut))
[PROOFSTEP]
filter_upwards [h'φ] with i hi x
[GOAL]
case h
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ✝ : ContDiffBump 0
x₀✝ : G
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : IsOpenPosMeasure μ
inst✝¹ : FiniteDimensional ℝ G
inst✝ : IsAddLeftInvariant μ
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g
this✝ : IsAddHaarMeasure μ
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[Ioi 0] 0)
this : Tendsto (fun x => ⨍ (y : G) in closedBall x₀ (φ x).rOut, ‖g y - g x₀‖ ∂μ) l (𝓝 0)
i : ι
hi : (φ i).rOut ≤ K * (φ i).rIn
x : G
⊢ |ContDiffBump.normed (φ i) μ (x₀ - x)| ≤
    K ^ FiniteDimensional.finrank ℝ G / ENNReal.toReal (↑↑μ (closedBall x₀ (φ i).rOut))
[PROOFSTEP]
rw [abs_of_nonneg (nonneg_normed _ _), addHaar_closedBall_center]
[GOAL]
case h
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ✝ : ContDiffBump 0
x₀✝ : G
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : IsOpenPosMeasure μ
inst✝¹ : FiniteDimensional ℝ G
inst✝ : IsAddLeftInvariant μ
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g
this✝ : IsAddHaarMeasure μ
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[Ioi 0] 0)
this : Tendsto (fun x => ⨍ (y : G) in closedBall x₀ (φ x).rOut, ‖g y - g x₀‖ ∂μ) l (𝓝 0)
i : ι
hi : (φ i).rOut ≤ K * (φ i).rIn
x : G
⊢ ContDiffBump.normed (φ i) μ (x₀ - x) ≤
    K ^ FiniteDimensional.finrank ℝ G / ENNReal.toReal (↑↑μ (closedBall 0 (φ i).rOut))
[PROOFSTEP]
exact (φ i).normed_le_div_measure_closedBall_rOut _ _ hi _


[GOAL]
p : ℝ[X]
⊢ Finset.card (Multiset.toFinset (roots p)) ≤
    Finset.card (Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)) + 1
[PROOFSTEP]
cases' eq_or_ne (derivative p) 0 with hp' hp'
[GOAL]
case inl
p : ℝ[X]
hp' : ↑derivative p = 0
⊢ Finset.card (Multiset.toFinset (roots p)) ≤
    Finset.card (Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)) + 1
[PROOFSTEP]
rw [eq_C_of_derivative_eq_zero hp', roots_C, Multiset.toFinset_zero, Finset.card_empty]
[GOAL]
case inl
p : ℝ[X]
hp' : ↑derivative p = 0
⊢ 0 ≤ Finset.card (Multiset.toFinset (roots (↑derivative (↑C (coeff p 0)))) \ ∅) + 1
[PROOFSTEP]
exact zero_le _
[GOAL]
case inr
p : ℝ[X]
hp' : ↑derivative p ≠ 0
⊢ Finset.card (Multiset.toFinset (roots p)) ≤
    Finset.card (Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)) + 1
[PROOFSTEP]
have hp : p ≠ 0 := ne_of_apply_ne derivative (by rwa [derivative_zero])
[GOAL]
p : ℝ[X]
hp' : ↑derivative p ≠ 0
⊢ ↑derivative p ≠ ↑derivative 0
[PROOFSTEP]
rwa [derivative_zero]
[GOAL]
case inr
p : ℝ[X]
hp' : ↑derivative p ≠ 0
hp : p ≠ 0
⊢ Finset.card (Multiset.toFinset (roots p)) ≤
    Finset.card (Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)) + 1
[PROOFSTEP]
refine' Finset.card_le_diff_of_interleaved fun x hx y hy hxy hxy' => _
[GOAL]
case inr
p : ℝ[X]
hp' : ↑derivative p ≠ 0
hp : p ≠ 0
x : ℝ
hx : x ∈ Multiset.toFinset (roots p)
y : ℝ
hy : y ∈ Multiset.toFinset (roots p)
hxy : x < y
hxy' : ∀ (z : ℝ), z ∈ Multiset.toFinset (roots p) → ¬z ∈ Set.Ioo x y
⊢ ∃ z, z ∈ Multiset.toFinset (roots (↑derivative p)) ∧ x < z ∧ z < y
[PROOFSTEP]
rw [Multiset.mem_toFinset, mem_roots hp] at hx hy
[GOAL]
case inr
p : ℝ[X]
hp' : ↑derivative p ≠ 0
hp : p ≠ 0
x : ℝ
hx : IsRoot p x
y : ℝ
hy : IsRoot p y
hxy : x < y
hxy' : ∀ (z : ℝ), z ∈ Multiset.toFinset (roots p) → ¬z ∈ Set.Ioo x y
⊢ ∃ z, z ∈ Multiset.toFinset (roots (↑derivative p)) ∧ x < z ∧ z < y
[PROOFSTEP]
obtain ⟨z, hz1, hz2⟩ := exists_deriv_eq_zero hxy p.continuousOn (hx.trans hy.symm)
[GOAL]
case inr.intro.intro
p : ℝ[X]
hp' : ↑derivative p ≠ 0
hp : p ≠ 0
x : ℝ
hx : IsRoot p x
y : ℝ
hy : IsRoot p y
hxy : x < y
hxy' : ∀ (z : ℝ), z ∈ Multiset.toFinset (roots p) → ¬z ∈ Set.Ioo x y
z : ℝ
hz1 : z ∈ Set.Ioo x y
hz2 : deriv (fun x => eval x p) z = 0
⊢ ∃ z, z ∈ Multiset.toFinset (roots (↑derivative p)) ∧ x < z ∧ z < y
[PROOFSTEP]
refine' ⟨z, _, hz1⟩
[GOAL]
case inr.intro.intro
p : ℝ[X]
hp' : ↑derivative p ≠ 0
hp : p ≠ 0
x : ℝ
hx : IsRoot p x
y : ℝ
hy : IsRoot p y
hxy : x < y
hxy' : ∀ (z : ℝ), z ∈ Multiset.toFinset (roots p) → ¬z ∈ Set.Ioo x y
z : ℝ
hz1 : z ∈ Set.Ioo x y
hz2 : deriv (fun x => eval x p) z = 0
⊢ z ∈ Multiset.toFinset (roots (↑derivative p))
[PROOFSTEP]
rwa [Multiset.mem_toFinset, mem_roots hp', IsRoot, ← p.deriv]
[GOAL]
p : ℝ[X]
⊢ ∑ x in Multiset.toFinset (roots p), (Multiset.count x (roots p) - 1 + 1) =
    ∑ x in Multiset.toFinset (roots p), (rootMultiplicity x p - 1) + Finset.card (Multiset.toFinset (roots p))
[PROOFSTEP]
simp only [Finset.sum_add_distrib, Finset.card_eq_sum_ones, count_roots]
[GOAL]
p : ℝ[X]
⊢ ∑ x in Multiset.toFinset (roots p), rootMultiplicity x (↑derivative p) +
      (Finset.card (Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)) + 1) ≤
    ∑ x in Multiset.toFinset (roots p), Multiset.count x (roots (↑derivative p)) +
      (∑ x in Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p),
          Multiset.count x (roots (↑derivative p)) +
        1)
[PROOFSTEP]
simp only [← count_roots]
[GOAL]
p : ℝ[X]
⊢ ∑ x in Multiset.toFinset (roots p), Multiset.count x (roots (↑derivative p)) +
      (Finset.card (Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)) + 1) ≤
    ∑ x in Multiset.toFinset (roots p), Multiset.count x (roots (↑derivative p)) +
      (∑ x in Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p),
          Multiset.count x (roots (↑derivative p)) +
        1)
[PROOFSTEP]
refine' add_le_add_left (add_le_add_right ((Finset.card_eq_sum_ones _).trans_le _) _) _
[GOAL]
p : ℝ[X]
⊢ ∑ x in Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p), 1 ≤
    ∑ x in Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p),
      Multiset.count x (roots (↑derivative p))
[PROOFSTEP]
refine' Finset.sum_le_sum fun x hx => Nat.succ_le_iff.2 <| _
[GOAL]
p : ℝ[X]
x : ℝ
hx : x ∈ Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)
⊢ 0 < Multiset.count x (roots (↑derivative p))
[PROOFSTEP]
rw [Multiset.count_pos, ← Multiset.mem_toFinset]
[GOAL]
p : ℝ[X]
x : ℝ
hx : x ∈ Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)
⊢ x ∈ Multiset.toFinset (roots (↑derivative p))
[PROOFSTEP]
exact (Finset.mem_sdiff.1 hx).1
[GOAL]
p : ℝ[X]
⊢ ∑ x in Multiset.toFinset (roots p), Multiset.count x (roots (↑derivative p)) +
      (∑ x in Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p),
          Multiset.count x (roots (↑derivative p)) +
        1) =
    ↑Multiset.card (roots (↑derivative p)) + 1
[PROOFSTEP]
rw [← add_assoc, ← Finset.sum_union Finset.disjoint_sdiff, Finset.union_sdiff_self_eq_union, ←
  Multiset.toFinset_sum_count_eq, ← Finset.sum_subset (Finset.subset_union_right _ _)]
[GOAL]
p : ℝ[X]
⊢ ∀ (x : ℝ),
    x ∈ Multiset.toFinset (roots p) ∪ Multiset.toFinset (roots (↑derivative p)) →
      ¬x ∈ Multiset.toFinset (roots (↑derivative p)) → Multiset.count x (roots (↑derivative p)) = 0
[PROOFSTEP]
intro x _ hx₂
[GOAL]
p : ℝ[X]
x : ℝ
a✝ : x ∈ Multiset.toFinset (roots p) ∪ Multiset.toFinset (roots (↑derivative p))
hx₂ : ¬x ∈ Multiset.toFinset (roots (↑derivative p))
⊢ Multiset.count x (roots (↑derivative p)) = 0
[PROOFSTEP]
simpa only [Multiset.mem_toFinset, Multiset.count_eq_zero] using hx₂
[GOAL]
F : Type u_1
inst✝¹ : CommRing F
inst✝ : Algebra F ℝ
p : F[X]
⊢ Fintype.card ↑(rootSet p ℝ) ≤ Fintype.card ↑(rootSet (↑derivative p) ℝ) + 1
[PROOFSTEP]
simpa only [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe, derivative_map] using
  card_roots_toFinset_le_derivative (p.map (algebraMap F ℝ))


[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : HasContDiffBump E
inst✝ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
x : E
⊢ ContDiffBump.normed f μ (c - x) = ContDiffBump.normed f μ (c + x)
[PROOFSTEP]
simp_rw [f.normed_def, f.sub]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : HasContDiffBump E
inst✝ : MeasurableSpace E
c : E
f✝ : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
f : ContDiffBump 0
x : E
⊢ ContDiffBump.normed f μ (-x) = ContDiffBump.normed f μ x
[PROOFSTEP]
simp_rw [f.normed_def, f.neg]
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ 0 < ∫ (x : E), ↑f x ∂μ
[PROOFSTEP]
refine' (integral_pos_iff_support_of_nonneg f.nonneg' f.integrable).mpr _
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ 0 < ↑↑μ (support fun i => ↑f i)
[PROOFSTEP]
rw [f.support_eq]
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ 0 < ↑↑μ (ball c f.rOut)
[PROOFSTEP]
exact measure_ball_pos μ c f.rOut_pos
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ ∫ (x : E), ContDiffBump.normed f μ x ∂μ = 1
[PROOFSTEP]
simp_rw [ContDiffBump.normed, div_eq_mul_inv, mul_comm (f _), ← smul_eq_mul, integral_smul]
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ (∫ (x : E), ↑f x ∂μ)⁻¹ • ∫ (x : E), ↑f x ∂μ = 1
[PROOFSTEP]
exact inv_mul_cancel f.integral_pos.ne'
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ support (ContDiffBump.normed f μ) = ball c f.rOut
[PROOFSTEP]
unfold ContDiffBump.normed
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ (support fun x => ↑f x / ∫ (x : E), ↑f x ∂μ) = ball c f.rOut
[PROOFSTEP]
rw [support_div, f.support_eq, support_const f.integral_pos.ne', inter_univ]
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ tsupport (ContDiffBump.normed f μ) = closedBall c f.rOut
[PROOFSTEP]
rw [tsupport, f.support_normed_eq, closure_ball _ f.rOut_pos.ne']
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ HasCompactSupport (ContDiffBump.normed f μ)
[PROOFSTEP]
simp only [HasCompactSupport, f.tsupport_normed_eq (μ := μ), isCompact_closedBall]
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
ι : Type u_2
φ : ι → ContDiffBump c
l : Filter ι
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
⊢ Tendsto (fun i => support fun x => ContDiffBump.normed (φ i) μ x) l (smallSets (𝓝 c))
[PROOFSTEP]
simp_rw [NormedAddCommGroup.tendsto_nhds_zero, Real.norm_eq_abs, abs_eq_self.mpr (φ _).rOut_pos.le] at hφ
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
ι : Type u_2
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : ι) in l, (φ x).rOut < ε
⊢ Tendsto (fun i => support fun x => ContDiffBump.normed (φ i) μ x) l (smallSets (𝓝 c))
[PROOFSTEP]
rw [nhds_basis_ball.smallSets.tendsto_right_iff]
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
ι : Type u_2
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : ι) in l, (φ x).rOut < ε
⊢ ∀ (i : ℝ), 0 < i → ∀ᶠ (x : ι) in l, (support fun x_1 => ContDiffBump.normed (φ x) μ x_1) ∈ 𝒫 ball c i
[PROOFSTEP]
refine fun ε hε ↦ (hφ ε hε).mono fun i hi ↦ ?_
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
ι : Type u_2
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : ι) in l, (φ x).rOut < ε
ε : ℝ
hε : 0 < ε
i : ι
hi : (φ i).rOut < ε
⊢ (support fun x => ContDiffBump.normed (φ i) μ x) ∈ 𝒫 ball c ε
[PROOFSTEP]
rw [(φ i).support_normed_eq]
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
ι : Type u_2
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : ι) in l, (φ x).rOut < ε
ε : ℝ
hε : 0 < ε
i : ι
hi : (φ i).rOut < ε
⊢ ball c (φ i).rOut ∈ 𝒫 ball c ε
[PROOFSTEP]
exact ball_subset_ball hi.le
[GOAL]
E : Type u_1
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : HasContDiffBump E
inst✝⁷ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝⁶ : BorelSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : IsLocallyFiniteMeasure μ
inst✝³ : IsOpenPosMeasure μ
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : CompleteSpace X
z : X
⊢ ∫ (x : E), ContDiffBump.normed f μ x • z ∂μ = z
[PROOFSTEP]
simp_rw [integral_smul_const, f.integral_normed (μ := μ), one_smul]
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ ENNReal.toReal (↑↑μ (closedBall c f.rIn)) ≤ ∫ (x : E), ↑f x ∂μ
[PROOFSTEP]
calc
  (μ (closedBall c f.rIn)).toReal = ∫ x in closedBall c f.rIn, 1 ∂μ := by simp
  _ = ∫ x in closedBall c f.rIn, f x ∂μ :=
    (set_integral_congr (measurableSet_closedBall) (fun x hx ↦ (one_of_mem_closedBall f hx).symm))
  _ ≤ ∫ x, f x ∂μ := set_integral_le_integral f.integrable (eventually_of_forall (fun x ↦ f.nonneg))
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ ENNReal.toReal (↑↑μ (closedBall c f.rIn)) = ∫ (x : E) in closedBall c f.rIn, 1 ∂μ
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
x : E
⊢ ContDiffBump.normed f μ x ≤ 1 / ENNReal.toReal (↑↑μ (closedBall c f.rIn))
[PROOFSTEP]
rw [normed_def]
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
x : E
⊢ ↑f x / ∫ (x : E), ↑f x ∂μ ≤ 1 / ENNReal.toReal (↑↑μ (closedBall c f.rIn))
[PROOFSTEP]
gcongr
[GOAL]
case hd
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
x : E
⊢ 0 < ENNReal.toReal (↑↑μ (closedBall c f.rIn))
[PROOFSTEP]
exact ENNReal.toReal_pos (measure_closedBall_pos _ _ f.rIn_pos).ne' measure_closedBall_lt_top.ne
[GOAL]
case hac
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
x : E
⊢ ↑f x ≤ 1
[PROOFSTEP]
exact f.le_one
[GOAL]
case hbd
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
x : E
⊢ ENNReal.toReal (↑↑μ (closedBall c f.rIn)) ≤ ∫ (x : E), ↑f x ∂μ
[PROOFSTEP]
exact f.measure_closedBall_le_integral μ
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ ∫ (x : E), ↑f x ∂μ ≤ ENNReal.toReal (↑↑μ (closedBall c f.rOut))
[PROOFSTEP]
calc
  ∫ x, f x ∂μ = ∫ x in closedBall c f.rOut, f x ∂μ :=
    by
    apply (set_integral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm
    apply f.zero_of_le_dist (le_of_lt _)
    simpa using hx
  _ ≤ ∫ x in closedBall c f.rOut, 1 ∂μ :=
    by
    apply set_integral_mono f.integrable.integrableOn _ (fun x ↦ f.le_one)
    simp [measure_closedBall_lt_top]
  _ = (μ (closedBall c f.rOut)).toReal := by simp
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ ∫ (x : E), ↑f x ∂μ = ∫ (x : E) in closedBall c f.rOut, ↑f x ∂μ
[PROOFSTEP]
apply (set_integral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
x : E
hx : ¬x ∈ closedBall c f.rOut
⊢ ↑f x = 0
[PROOFSTEP]
apply f.zero_of_le_dist (le_of_lt _)
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
x : E
hx : ¬x ∈ closedBall c f.rOut
⊢ f.rOut < dist x c
[PROOFSTEP]
simpa using hx
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ ∫ (x : E) in closedBall c f.rOut, ↑f x ∂μ ≤ ∫ (x : E) in closedBall c f.rOut, 1 ∂μ
[PROOFSTEP]
apply set_integral_mono f.integrable.integrableOn _ (fun x ↦ f.le_one)
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ IntegrableOn (fun x => 1) (closedBall c f.rOut)
[PROOFSTEP]
simp [measure_closedBall_lt_top]
[GOAL]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
⊢ ∫ (x : E) in closedBall c f.rOut, 1 ∂μ = ENNReal.toReal (↑↑μ (closedBall c f.rOut))
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
⊢ ENNReal.toReal (↑↑μ (closedBall c f.rOut)) / K ^ finrank ℝ E ≤ ∫ (x : E), ↑f x ∂μ
[PROOFSTEP]
have K_pos : 0 < K := by simpa [f.rIn_pos, not_lt.2 f.rIn_pos.le] using mul_pos_iff.1 (f.rOut_pos.trans_le h)
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
⊢ 0 < K
[PROOFSTEP]
simpa [f.rIn_pos, not_lt.2 f.rIn_pos.le] using mul_pos_iff.1 (f.rOut_pos.trans_le h)
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
⊢ ENNReal.toReal (↑↑μ (closedBall c f.rOut)) / K ^ finrank ℝ E ≤ ∫ (x : E), ↑f x ∂μ
[PROOFSTEP]
apply le_trans _ (f.measure_closedBall_le_integral μ)
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
⊢ ENNReal.toReal (↑↑μ (closedBall c f.rOut)) / K ^ finrank ℝ E ≤ ENNReal.toReal (↑↑μ (closedBall c f.rIn))
[PROOFSTEP]
rw [div_le_iff (pow_pos K_pos _), addHaar_closedBall' _ _ f.rIn_pos.le, addHaar_closedBall' _ _ f.rOut_pos.le,
  ENNReal.toReal_mul, ENNReal.toReal_mul, ENNReal.toReal_ofReal (pow_nonneg f.rOut_pos.le _),
  ENNReal.toReal_ofReal (pow_nonneg f.rIn_pos.le _), mul_assoc, mul_comm _ (K ^ _), ← mul_assoc, ← mul_pow,
  mul_comm _ K]
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
⊢ f.rOut ^ finrank ℝ E * ENNReal.toReal (↑↑μ (closedBall 0 1)) ≤
    (K * f.rIn) ^ finrank ℝ E * ENNReal.toReal (↑↑μ (closedBall 0 1))
[PROOFSTEP]
gcongr
[GOAL]
case h.ha
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
⊢ 0 ≤ f.rOut
[PROOFSTEP]
exact f.rOut_pos.le
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
⊢ ContDiffBump.normed f μ x ≤ K ^ finrank ℝ E / ENNReal.toReal (↑↑μ (closedBall c f.rOut))
[PROOFSTEP]
have K_pos : 0 < K := by simpa [f.rIn_pos, not_lt.2 f.rIn_pos.le] using mul_pos_iff.1 (f.rOut_pos.trans_le h)
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
⊢ 0 < K
[PROOFSTEP]
simpa [f.rIn_pos, not_lt.2 f.rIn_pos.le] using mul_pos_iff.1 (f.rOut_pos.trans_le h)
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
⊢ ContDiffBump.normed f μ x ≤ K ^ finrank ℝ E / ENNReal.toReal (↑↑μ (closedBall c f.rOut))
[PROOFSTEP]
have : f x / ∫ y, f y ∂μ ≤ 1 / ∫ y, f y ∂μ := by
  gcongr
  · exact f.integral_pos.le
  · exact f.le_one
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
⊢ ↑f x / ∫ (y : E), ↑f y ∂μ ≤ 1 / ∫ (y : E), ↑f y ∂μ
[PROOFSTEP]
gcongr
[GOAL]
case hc
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
⊢ 0 ≤ ∫ (y : E), ↑f y ∂μ
[PROOFSTEP]
exact f.integral_pos.le
[GOAL]
case h
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
⊢ ↑f x ≤ 1
[PROOFSTEP]
exact f.le_one
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
this : ↑f x / ∫ (y : E), ↑f y ∂μ ≤ 1 / ∫ (y : E), ↑f y ∂μ
⊢ ContDiffBump.normed f μ x ≤ K ^ finrank ℝ E / ENNReal.toReal (↑↑μ (closedBall c f.rOut))
[PROOFSTEP]
apply this.trans
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
this : ↑f x / ∫ (y : E), ↑f y ∂μ ≤ 1 / ∫ (y : E), ↑f y ∂μ
⊢ 1 / ∫ (y : E), ↑f y ∂μ ≤ K ^ finrank ℝ E / ENNReal.toReal (↑↑μ (closedBall c f.rOut))
[PROOFSTEP]
rw [div_le_div_iff f.integral_pos, one_mul, ← div_le_iff' (pow_pos K_pos _)]
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
this : ↑f x / ∫ (y : E), ↑f y ∂μ ≤ 1 / ∫ (y : E), ↑f y ∂μ
⊢ ENNReal.toReal (↑↑μ (closedBall c f.rOut)) / K ^ finrank ℝ E ≤ ∫ (x : E), ↑f x ∂μ
[PROOFSTEP]
exact f.measure_closedBall_div_le_integral μ K h
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : HasContDiffBump E
inst✝⁵ : MeasurableSpace E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
μ : Measure E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsAddHaarMeasure μ
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
this : ↑f x / ∫ (y : E), ↑f y ∂μ ≤ 1 / ∫ (y : E), ↑f y ∂μ
⊢ 0 < ENNReal.toReal (↑↑μ (closedBall c f.rOut))
[PROOFSTEP]
exact ENNReal.toReal_pos (measure_closedBall_pos _ _ f.rOut_pos).ne' measure_closedBall_lt_top.ne


[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f'✝ f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
f' : 𝕜 →L[𝕜] F
⊢ HasFDerivAtFilter f f' x L ↔ HasDerivAtFilter f (↑f' 1) x L
[PROOFSTEP]
simp [HasDerivAtFilter]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f'✝ f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
f' : 𝕜 →L[𝕜] F
⊢ HasStrictFDerivAt f f' x ↔ HasStrictDerivAt f (↑f' 1) x
[PROOFSTEP]
simp [HasStrictDerivAt, HasStrictFDerivAt]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin f s x = 0
[PROOFSTEP]
unfold derivWithin
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ ↑(fderivWithin 𝕜 f s x) 1 = 0
[PROOFSTEP]
rw [fderivWithin_zero_of_not_differentiableWithinAt h]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ ↑0 1 = 0
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
h : ¬DifferentiableAt 𝕜 f x
⊢ deriv f x = 0
[PROOFSTEP]
unfold deriv
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
h : ¬DifferentiableAt 𝕜 f x
⊢ ↑(fderiv 𝕜 f x) 1 = 0
[PROOFSTEP]
rw [fderiv_zero_of_not_differentiableAt h]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
h : ¬DifferentiableAt 𝕜 f x
⊢ ↑0 1 = 0
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
hf : HasDerivAtFilter f f' x✝ L
hf' : f' ≠ 0
x : 𝕜
⊢ ‖x‖ ≤ ↑‖f'‖₊⁻¹ * ‖↑(smulRight 1 f') x‖
[PROOFSTEP]
simp [norm_smul, ← div_eq_inv_mul, mul_div_cancel _ (mt norm_eq_zero.1 hf')]
[GOAL]
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
inst✝ : PartialOrder 𝕜
⊢ HasDerivWithinAt f f' (Ioi x) x ↔ HasDerivWithinAt f f' (Ici x) x
[PROOFSTEP]
rw [← Ici_diff_left, hasDerivWithinAt_diff_singleton]
[GOAL]
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
inst✝ : PartialOrder 𝕜
⊢ HasDerivWithinAt f f' (Iio x) x ↔ HasDerivWithinAt f f' (Iic x) x
[PROOFSTEP]
rw [← Iic_diff_right, hasDerivWithinAt_diff_singleton]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
⊢ smulRight 1 (derivWithin f s x) = fderivWithin 𝕜 f s x
[PROOFSTEP]
simp [derivWithin]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
⊢ smulRight 1 (deriv f x) = fderiv 𝕜 f x
[PROOFSTEP]
simp [deriv]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
h : DifferentiableAt 𝕜 f x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ _root_.derivWithin f s x = deriv f x
[PROOFSTEP]
unfold derivWithin deriv
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
h : DifferentiableAt 𝕜 f x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ ↑(fderivWithin 𝕜 f s x) 1 = ↑(fderiv 𝕜 f x) 1
[PROOFSTEP]
rw [h.fderivWithin hxs]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
y : 𝕜
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ derivWithin f s x = derivWithin f t x
[PROOFSTEP]
simp only [derivWithin, fderivWithin_congr_set' y h]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
h : s =ᶠ[𝓝 x] t
⊢ derivWithin f s x = derivWithin f t x
[PROOFSTEP]
simp only [derivWithin, fderivWithin_congr_set h]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
⊢ derivWithin f univ = deriv f
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
x✝ : 𝕜
⊢ derivWithin f univ x✝ = deriv f x✝
[PROOFSTEP]
unfold derivWithin deriv
[GOAL]
case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
x✝ : 𝕜
⊢ ↑(fderivWithin 𝕜 f univ x✝) 1 = ↑(fderiv 𝕜 f x✝) 1
[PROOFSTEP]
rw [fderivWithin_univ]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
ht : t ∈ 𝓝 x
⊢ derivWithin f (s ∩ t) x = derivWithin f s x
[PROOFSTEP]
unfold derivWithin
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
ht : t ∈ 𝓝 x
⊢ ↑(fderivWithin 𝕜 f (s ∩ t) x) 1 = ↑(fderivWithin 𝕜 f s x) 1
[PROOFSTEP]
rw [fderivWithin_inter ht]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
hs : IsOpen s
hx : x ∈ s
⊢ derivWithin f s x = deriv f x
[PROOFSTEP]
unfold derivWithin
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
hs : IsOpen s
hx : x ∈ s
⊢ ↑(fderivWithin 𝕜 f s x) 1 = deriv f x
[PROOFSTEP]
rw [fderivWithin_of_open hs hx]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
hs : IsOpen s
hx : x ∈ s
⊢ ↑(fderiv 𝕜 f x) 1 = deriv f x
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f✝ f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s✝ t : Set 𝕜
L L₁ L₂ : Filter 𝕜
f : 𝕜 → F
s : Set F
x : 𝕜
⊢ deriv f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ deriv f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
[PROOFSTEP]
by_cases hx : DifferentiableAt 𝕜 f x
[GOAL]
case pos
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f✝ f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s✝ t : Set 𝕜
L L₁ L₂ : Filter 𝕜
f : 𝕜 → F
s : Set F
x : 𝕜
hx : DifferentiableAt 𝕜 f x
⊢ deriv f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ deriv f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
[PROOFSTEP]
simp [deriv_zero_of_not_differentiableAt, *]
[GOAL]
case neg
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f✝ f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s✝ t : Set 𝕜
L L₁ L₂ : Filter 𝕜
f : 𝕜 → F
s : Set F
x : 𝕜
hx : ¬DifferentiableAt 𝕜 f x
⊢ deriv f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ deriv f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
[PROOFSTEP]
simp [deriv_zero_of_not_differentiableAt, *]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f✝ f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s✝ t✝ : Set 𝕜
L L₁ L₂ : Filter 𝕜
f : 𝕜 → F
t : Set 𝕜
s : Set F
x : 𝕜
⊢ derivWithin f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ derivWithin f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s
[PROOFSTEP]
by_cases hx : DifferentiableWithinAt 𝕜 f t x
[GOAL]
case pos
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f✝ f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s✝ t✝ : Set 𝕜
L L₁ L₂ : Filter 𝕜
f : 𝕜 → F
t : Set 𝕜
s : Set F
x : 𝕜
hx : DifferentiableWithinAt 𝕜 f t x
⊢ derivWithin f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ derivWithin f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s
[PROOFSTEP]
simp [derivWithin_zero_of_not_differentiableWithinAt, *]
[GOAL]
case neg
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f✝ f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s✝ t✝ : Set 𝕜
L L₁ L₂ : Filter 𝕜
f : 𝕜 → F
t : Set 𝕜
s : Set F
x : 𝕜
hx : ¬DifferentiableWithinAt 𝕜 f t x
⊢ derivWithin f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ derivWithin f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s
[PROOFSTEP]
simp [derivWithin_zero_of_not_differentiableWithinAt, *]
[GOAL]
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E✝ : Type w
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace 𝕜 E✝
f✝ f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x
[PROOFSTEP]
by_cases H : DifferentiableWithinAt ℝ f (Ioi x) x
[GOAL]
case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E✝ : Type w
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace 𝕜 E✝
f✝ f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : DifferentiableWithinAt ℝ f (Ioi x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x
[PROOFSTEP]
have A := H.hasDerivWithinAt.Ici_of_Ioi
[GOAL]
case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E✝ : Type w
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace 𝕜 E✝
f✝ f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : DifferentiableWithinAt ℝ f (Ioi x) x
A : HasDerivWithinAt f (derivWithin f (Ioi x) x) (Ici x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x
[PROOFSTEP]
have B := (differentiableWithinAt_Ioi_iff_Ici.1 H).hasDerivWithinAt
[GOAL]
case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E✝ : Type w
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace 𝕜 E✝
f✝ f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : DifferentiableWithinAt ℝ f (Ioi x) x
A : HasDerivWithinAt f (derivWithin f (Ioi x) x) (Ici x) x
B : HasDerivWithinAt f (derivWithin f (Ici x) x) (Ici x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x
[PROOFSTEP]
simpa using (uniqueDiffOn_Ici x).eq left_mem_Ici A B
[GOAL]
case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E✝ : Type w
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace 𝕜 E✝
f✝ f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : ¬DifferentiableWithinAt ℝ f (Ioi x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x
[PROOFSTEP]
rw [derivWithin_zero_of_not_differentiableWithinAt H, derivWithin_zero_of_not_differentiableWithinAt]
[GOAL]
case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E✝ : Type w
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace 𝕜 E✝
f✝ f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : ¬DifferentiableWithinAt ℝ f (Ioi x) x
⊢ ¬DifferentiableWithinAt ℝ f (Ici x) x
[PROOFSTEP]
rwa [differentiableWithinAt_Ioi_iff_Ici] at H
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
h₀ : f₀ =ᶠ[L] f₁
hx : f₀ x = f₁ x
h₁ : f₀' = f₁'
⊢ ∀ (x : 𝕜), ↑(smulRight 1 f₀') x = ↑(smulRight 1 f₁') x
[PROOFSTEP]
simp [h₁]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
h : HasDerivAtFilter f f' x L
hL : f₁ =ᶠ[L] f
hx : f₁ x = f x
⊢ HasDerivAtFilter f₁ f' x L
[PROOFSTEP]
rwa [hL.hasDerivAtFilter_iff hx rfl]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ derivWithin f₁ s x = derivWithin f s x
[PROOFSTEP]
unfold derivWithin
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ ↑(fderivWithin 𝕜 f₁ s x) 1 = ↑(fderivWithin 𝕜 f s x) 1
[PROOFSTEP]
rw [hs.fderivWithin_eq hx]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
hs : EqOn f₁ f s
hx : f₁ x = f x
⊢ derivWithin f₁ s x = derivWithin f s x
[PROOFSTEP]
unfold derivWithin
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
hs : EqOn f₁ f s
hx : f₁ x = f x
⊢ ↑(fderivWithin 𝕜 f₁ s x) 1 = ↑(fderivWithin 𝕜 f s x) 1
[PROOFSTEP]
rw [fderivWithin_congr hs hx]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
hL : f₁ =ᶠ[𝓝 x] f
⊢ deriv f₁ x = deriv f x
[PROOFSTEP]
unfold deriv
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
hL : f₁ =ᶠ[𝓝 x] f
⊢ ↑(fderiv 𝕜 f₁ x) 1 = ↑(fderiv 𝕜 f x) 1
[PROOFSTEP]
rwa [Filter.EventuallyEq.fderiv_eq]


[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
⊢ Monotone fun s => posTangentConeAt s a
[PROOFSTEP]
rintro s t hst y ⟨c, d, hd, hc, hcd⟩
[GOAL]
case intro.intro.intro.intro
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s t : Set E
hst : s ≤ t
y : E
c : ℕ → ℝ
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
⊢ y ∈ (fun s => posTangentConeAt s a) t
[PROOFSTEP]
exact ⟨c, d, mem_of_superset hd fun h hn => hst hn, hc, hcd⟩
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x y ⊆ s
⊢ y - x ∈ posTangentConeAt s x
[PROOFSTEP]
let c := fun n : ℕ => (2 : ℝ) ^ n
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ n
⊢ y - x ∈ posTangentConeAt s x
[PROOFSTEP]
let d := fun n : ℕ => (c n)⁻¹ • (y - x)
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ n
d : ℕ → E := fun n => (c n)⁻¹ • (y - x)
⊢ y - x ∈ posTangentConeAt s x
[PROOFSTEP]
refine' ⟨c, d, Filter.univ_mem' fun n => h _, tendsto_pow_atTop_atTop_of_one_lt one_lt_two, _⟩
[GOAL]
case refine'_1
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ n
d : ℕ → E := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ x + d n ∈ segment ℝ x y
case refine'_2
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ n
d : ℕ → E := fun n => (c n)⁻¹ • (y - x)
⊢ Tendsto (fun n => c n • d n) atTop (𝓝 (y - x))
[PROOFSTEP]
show x + d n ∈ segment ℝ x y
[GOAL]
case refine'_1
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ n
d : ℕ → E := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ x + d n ∈ segment ℝ x y
[PROOFSTEP]
rw [segment_eq_image']
[GOAL]
case refine'_1
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ n
d : ℕ → E := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ x + d n ∈ (fun θ => x + θ • (y - x)) '' Icc 0 1
[PROOFSTEP]
refine' ⟨(c n)⁻¹, ⟨_, _⟩, rfl⟩
[GOAL]
case refine'_1.refine'_1
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ n
d : ℕ → E := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ 0 ≤ (c n)⁻¹
case refine'_1.refine'_2
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ n
d : ℕ → E := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ (c n)⁻¹ ≤ 1
[PROOFSTEP]
exacts [inv_nonneg.2 (pow_nonneg zero_le_two _), inv_le_one (one_le_pow_of_one_le one_le_two _)]
[GOAL]
case refine'_2
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ n
d : ℕ → E := fun n => (c n)⁻¹ • (y - x)
⊢ Tendsto (fun n => c n • d n) atTop (𝓝 (y - x))
[PROOFSTEP]
show Tendsto (fun n => c n • d n) atTop (𝓝 (y - x))
[GOAL]
case refine'_2
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ n
d : ℕ → E := fun n => (c n)⁻¹ • (y - x)
⊢ Tendsto (fun n => c n • d n) atTop (𝓝 (y - x))
[PROOFSTEP]
exact tendsto_const_nhds.congr fun n ↦ (smul_inv_smul₀ (pow_ne_zero _ two_ne_zero) _).symm
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x (x + y) ⊆ s
⊢ y ∈ posTangentConeAt s x
[PROOFSTEP]
simpa only [add_sub_cancel'] using mem_posTangentConeAt_of_segment_subset h
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
hy : y ∈ posTangentConeAt s a
⊢ ↑f' y ≤ 0
[PROOFSTEP]
rcases hy with ⟨c, d, hd, hc, hcd⟩
[GOAL]
case intro.intro.intro.intro
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
c : ℕ → ℝ
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
⊢ ↑f' y ≤ 0
[PROOFSTEP]
have hc' : Tendsto (‖c ·‖) atTop atTop := tendsto_abs_atTop_atTop.comp hc
[GOAL]
case intro.intro.intro.intro
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
c : ℕ → ℝ
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
hc' : Tendsto (fun x => ‖c x‖) atTop atTop
⊢ ↑f' y ≤ 0
[PROOFSTEP]
suffices : ∀ᶠ n in atTop, c n • (f (a + d n) - f a) ≤ 0
[GOAL]
case intro.intro.intro.intro
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
c : ℕ → ℝ
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
hc' : Tendsto (fun x => ‖c x‖) atTop atTop
this : ∀ᶠ (n : ℕ) in atTop, c n • (f (a + d n) - f a) ≤ 0
⊢ ↑f' y ≤ 0
[PROOFSTEP]
exact le_of_tendsto (hf.lim atTop hd hc' hcd) this
[GOAL]
case this
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
c : ℕ → ℝ
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
hc' : Tendsto (fun x => ‖c x‖) atTop atTop
⊢ ∀ᶠ (n : ℕ) in atTop, c n • (f (a + d n) - f a) ≤ 0
[PROOFSTEP]
replace hd : Tendsto (fun n => a + d n) atTop (𝓝[s] (a + 0))
[GOAL]
case hd
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
c : ℕ → ℝ
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
hc' : Tendsto (fun x => ‖c x‖) atTop atTop
⊢ Tendsto (fun n => a + d n) atTop (𝓝[s] (a + 0))
[PROOFSTEP]
exact tendsto_nhdsWithin_iff.2 ⟨tendsto_const_nhds.add (tangentConeAt.lim_zero _ hc' hcd), hd⟩
[GOAL]
case this
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
c : ℕ → ℝ
d : ℕ → E
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
hc' : Tendsto (fun x => ‖c x‖) atTop atTop
hd : Tendsto (fun n => a + d n) atTop (𝓝[s] (a + 0))
⊢ ∀ᶠ (n : ℕ) in atTop, c n • (f (a + d n) - f a) ≤ 0
[PROOFSTEP]
rw [add_zero] at hd
[GOAL]
case this
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
c : ℕ → ℝ
d : ℕ → E
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
hc' : Tendsto (fun x => ‖c x‖) atTop atTop
hd : Tendsto (fun n => a + d n) atTop (𝓝[s] a)
⊢ ∀ᶠ (n : ℕ) in atTop, c n • (f (a + d n) - f a) ≤ 0
[PROOFSTEP]
filter_upwards [hd.eventually h, hc.eventually_ge_atTop 0] with n hfn hcn
[GOAL]
case h
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
c : ℕ → ℝ
d : ℕ → E
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
hc' : Tendsto (fun x => ‖c x‖) atTop atTop
hd : Tendsto (fun n => a + d n) atTop (𝓝[s] a)
n : ℕ
hfn : f (a + d n) ≤ f a
hcn : 0 ≤ c n
⊢ c n • (f (a + d n) - f a) ≤ 0
[PROOFSTEP]
exact mul_nonpos_of_nonneg_of_nonpos hcn (sub_nonpos.2 hfn)
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
y : E
hy : y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ ↑(fderivWithin ℝ f s a) y ≤ 0
[PROOFSTEP]
rw [fderivWithin_zero_of_not_differentiableWithinAt hf]
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
y : E
hy : y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ ↑0 y ≤ 0
[PROOFSTEP]
rfl
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
⊢ 0 ≤ ↑f' y
[PROOFSTEP]
simpa using h.hasFDerivWithinAt_nonpos hf hy'
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
y : E
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ ↑(fderivWithin ℝ f s a) y = 0
[PROOFSTEP]
rw [fderivWithin_zero_of_not_differentiableWithinAt hf]
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
y : E
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ ↑0 y = 0
[PROOFSTEP]
rfl
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMinOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
hy : y ∈ posTangentConeAt s a
⊢ 0 ≤ ↑f' y
[PROOFSTEP]
simpa using h.neg.hasFDerivWithinAt_nonpos hf.neg hy
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMinOn f s a
y : E
hy : y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 ≤ ↑(fderivWithin ℝ f s a) y
[PROOFSTEP]
rw [fderivWithin_zero_of_not_differentiableWithinAt hf]
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMinOn f s a
y : E
hy : y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 ≤ ↑0 y
[PROOFSTEP]
rfl
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMinOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
⊢ ↑f' y = 0
[PROOFSTEP]
simpa using h.neg.hasFDerivWithinAt_eq_zero hf.neg hy hy'
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMinOn f s a
y : E
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ ↑(fderivWithin ℝ f s a) y = 0
[PROOFSTEP]
rw [fderivWithin_zero_of_not_differentiableWithinAt hf]
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMinOn f s a
y : E
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ ↑0 y = 0
[PROOFSTEP]
rfl
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
h : IsLocalMin f a
hf : HasFDerivAt f f' a
⊢ f' = 0
[PROOFSTEP]
ext y
[GOAL]
case h
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ ↑f' y = ↑0 y
[PROOFSTEP]
apply (h.on univ).hasFDerivWithinAt_eq_zero hf.hasFDerivWithinAt
[GOAL]
case h.hy
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ y ∈ posTangentConeAt univ a
[PROOFSTEP]
rw [posTangentConeAt_univ]
[GOAL]
case h.hy'
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ -y ∈ posTangentConeAt univ a
[PROOFSTEP]
rw [posTangentConeAt_univ]
[GOAL]
case h.hy
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ y ∈ univ
[PROOFSTEP]
apply mem_univ
[GOAL]
case h.hy'
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ -y ∈ univ
[PROOFSTEP]
apply mem_univ
[GOAL]
f : ℝ → ℝ
f' a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ f' = 0
[PROOFSTEP]
simpa using FunLike.congr_fun (h.hasFDerivAt_eq_zero (hasDerivAt_iff_hasFDerivAt.1 hf)) 1