Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution

Goal state before:
pp: case 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✝³ : CompleteSpace E'
inst✝² : BorelSpace G
inst✝¹ : FiniteDimensional ℝ G
inst✝ : μ.IsAddHaarMeasure
ι : 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
h₀ : Tendsto (fun a ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)
hφ' : Tendsto (fun i ↦ (φ i).rOut) l (𝓝[>] 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 ↦ ∫ (y : G), (φ i).normed μ (x₀ - y) ∂μ) l (𝓝 1)

pp: case 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✝³ : CompleteSpace E'
inst✝² : BorelSpace G
inst✝¹ : FiniteDimensional ℝ G
inst✝ : μ.IsAddHaarMeasure
ι : 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
h₀ : Tendsto (fun a ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)
hφ' : Tendsto (fun i ↦ (φ i).rOut) l (𝓝[>] 0)
this : Tendsto (((fun a ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun r ↦ closedBall x₀ r) ∘ fun i ↦ (φ i).rOut) l (𝓝 0)
⊢ ∀ᶠ (i : ι) in l, (support fun y ↦ (φ i).normed μ (x₀ - y)) ⊆ (fun r ↦ closedBall x₀ r) ((fun i ↦ (φ i).rOut) i)

pp: case 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✝³ : CompleteSpace E'
inst✝² : BorelSpace G
inst✝¹ : FiniteDimensional ℝ G
inst✝ : μ.IsAddHaarMeasure
ι : 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
h₀ : Tendsto (fun a ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)
hφ' : Tendsto (fun i ↦ (φ i).rOut) l (𝓝[>] 0)
this : Tendsto (((fun a ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun r ↦ closedBall x₀ r) ∘ fun i ↦ (φ i).rOut) l (𝓝 0)
⊢ ∀ᶠ (i : ι) in l,
    ∀ (x : G),
      |(φ i).normed μ (x₀ - x)| ≤ K ^ Module.finrank ℝ G / μ.real ((fun r ↦ closedBall x₀ r) ((fun i ↦ (φ i).rOut) i))

Tactic:
· apply tendsto_const_nhds.congr (fun i ↦ ?_)
    rw [← integral_neg_eq_self]
    simp only [sub_neg_eq_add, integral_add_left_eq_self, integral_normed]

Goal state after:
case 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✝³ : CompleteSpace E'
inst✝² : BorelSpace G
inst✝¹ : FiniteDimensional ℝ G
inst✝ : μ.IsAddHaarMeasure
ι : 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
h₀ : Tendsto (fun a ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)
hφ' : Tendsto (fun i ↦ (φ i).rOut) l (𝓝[>] 0)
this : Tendsto (((fun a ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun r ↦ closedBall x₀ r) ∘ fun i ↦ (φ i).rOut) l (𝓝 0)
⊢ ∀ᶠ (i : ι) in l, (support fun y ↦ (φ i).normed μ (x₀ - y)) ⊆ (fun r ↦ closedBall x₀ r) ((fun i ↦ (φ i).rOut) i)

case 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✝³ : CompleteSpace E'
inst✝² : BorelSpace G
inst✝¹ : FiniteDimensional ℝ G
inst✝ : μ.IsAddHaarMeasure
ι : 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
h₀ : Tendsto (fun a ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)
hφ' : Tendsto (fun i ↦ (φ i).rOut) l (𝓝[>] 0)
this : Tendsto (((fun a ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun r ↦ closedBall x₀ r) ∘ fun i ↦ (φ i).rOut) l (𝓝 0)
⊢ ∀ᶠ (i : ι) in l,
    ∀ (x : G),
      |(φ i).normed μ (x₀ - x)| ≤ K ^ Module.finrank ℝ G / μ.real ((fun r ↦ closedBall x₀ r) ((fun i ↦ (φ i).rOut) i))