[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 _
