awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convolution (hypothesis)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
t : G
ht : t ∉ support f
⊢ dist.{uF} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
      ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F) ≤
    norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
have ht₁ : f t = 0
Tactic: rw [notMem_support] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
t : G
ht : f t = 0
⊢ dist.{uF} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
      ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F) ≤
    norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
have neg : LE.le (α := ℝ) 0 0
Tactic: simp_rw [ht, L.map_zero₂, L.map_zero, norm_zero, zero_mul, dist_self]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (hypothesis)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
⊢ dist ((f ⋆[L, μ] g) x₀) (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ ∂μ) ≤
    (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
have h2 : ∀ (t : G),
  dist.{uF} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
      ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F) ≤
    norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
Tactic: have h2 : ∀ t, dist (L (f t) (g (x₀ - t))) (L (f t) z₀) ≤ ‖L (f t)‖ * ε := by
    intro t; by_cases ht : t ∈ support f
    · have h2t := hf ht
      rw [mem_ball_zero_iff] at h2t
      specialize hg (x₀ - t)
      rw [sub_eq_add_neg, add_mem_ball_iff_norm, norm_neg, ← sub_eq_add_neg] at hg
      refine ((L (f t)).dist_le_opNorm _ _).trans ?_
      gcongr
      exact hg h2t
    · rw [notMem_support] at ht
      simp_rw [ht, L.map_zero₂, L.map_zero, norm_zero, zero_mul, dist_self]
      rfl
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
h2 :
  ∀ (t : G),
    dist.{uF} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
        ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F) ≤
      norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
⊢ dist ((f ⋆[L, μ] g) x₀) (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ ∂μ) ≤
    (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
have simp_rw : dist.{uF} (α := F) (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) ∂μ)
    (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ ∂μ) ≤
  (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
Tactic: simp_rw [convolution_def]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
h2 :
  ∀ (t : G),
    dist.{uF} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
        ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F) ≤
      norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
⊢ dist.{uF} (α := F) (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) ∂μ)
      (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ ∂μ) ≤
    (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
have simp_rw : ∀
  (h2 :
    ∀ (t : G),
      ‖HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
            ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F)‖ ≤
        norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε),
  ‖HSub.hSub (α := F) (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) ∂μ)
        (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ ∂μ)‖ ≤
    (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
Tactic: simp_rw [dist_eq_norm] at h2 ⊢
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
h2 :
  ∀ (t : G),
    ‖HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F)‖ ≤
      norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
⊢ ‖HSub.hSub (α := F) (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) ∂μ)
        (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ ∂μ)‖ ≤
    (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
have rw : norm.{uF} (E := F)
    (∫ (a : G),
      HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - a)) : F)
        ((((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) z₀ : F) ∂μ) ≤
  (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
Tactic: rw [← integral_sub hfg.integrable]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
h2 :
  ∀ (t : G),
    ‖HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F)‖ ≤
      norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
rw :
  norm.{uF} (E := F)
      (∫ (a : G),
        HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - a)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) z₀ : F) ∂μ) ≤
    (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
⊢ ‖HSub.hSub (α := F) (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) ∂μ)
        (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ ∂μ)‖ ≤
    (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
have rw₁ : Integrable.{uF, uG} (ε := F) (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀) μ
Tactic: rw [← integral_sub hfg.integrable]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
h2 :
  ∀ (t : G),
    ‖HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F)‖ ≤
      norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
⊢ norm.{uF} (E := F)
      (∫ (a : G),
        HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - a)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) z₀ : F) ∂μ) ≤
    (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
have refine : ∫ (x : G), norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f x) : E' →L[𝕜] F) * ε ∂μ ≤
  (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
Tactic: refine (norm_integral_le_of_norm_le ((L.integrable_comp hif).norm.mul_const ε)
    (Eventually.of_forall h2)).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
h2 :
  ∀ (t : G),
    ‖HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F)‖ ≤
      norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
⊢ ∫ (x : G), norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f x) : E' →L[𝕜] F) * ε ∂μ ≤
    (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
have rw : (∫ (a : G), norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) ∂μ) * ε ≤
  (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
Tactic: rw [integral_mul_const]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
h2 :
  ∀ (t : G),
    ‖HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F)‖ ≤
      norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
⊢ (∫ (a : G), norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) ∂μ) * ε ≤
    (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
have hbc : ∫ (a : G), norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) ∂μ ≤ ‖L‖ * ∫ (x : G), ‖f x‖ ∂μ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convolution (hypothesis)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
h2 :
  ∀ (t : G),
    ‖HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F)‖ ≤
      norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
⊢ ∫ (a : G), norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) ∂μ ≤ ‖L‖ * ∫ (x : G), ‖f x‖ ∂μ
have h3 : ∀ (t : G), norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) ≤ ‖L‖ * ‖f t‖
Tactic: have h3 : ∀ t, ‖L (f t)‖ ≤ ‖L‖ * ‖f t‖ := by
    intro t
    exact L.le_opNorm (f t)
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
h2 :
  ∀ (t : G),
    ‖HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F)‖ ≤
      norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
h3 : ∀ (t : G), norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) ≤ ‖L‖ * ‖f t‖
⊢ ∫ (a : G), norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) ∂μ ≤ ‖L‖ * ∫ (x : G), ‖f x‖ ∂μ
have hbc : ∫ (x : G), ‖L‖ * ‖f x‖ ∂μ = ‖L‖ * ∫ (x : G), ‖f x‖ ∂μ
Tactic: refine (integral_mono (L.integrable_comp hif).norm (hif.norm.const_mul _) h3).trans_eq ?_
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
h2 :
  ∀ (t : G),
    ‖HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F)‖ ≤
      norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
h3 : ∀ (t : G), norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) ≤ ‖L‖ * ‖f t‖
⊢ ∫ (x : G), ‖L‖ * ‖f x‖ ∂μ = ‖L‖ * ∫ (x : G), ‖f x‖ ∂μ
have hbc : ‖L‖ * ∫ (a : G), ‖f a‖ ∂μ = ‖L‖ * ∫ (x : G), ‖f x‖ ∂μ
Tactic: rw [integral_const_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (hypothesis)
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : CompleteSpace E'
f : G → ℝ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hf : support f ⊆ ball 0 R
hnf : ∀ (x : G), 0 ≤ f x
hintf : Eq (α := ℝ) (∫ (x : G), f x ∂μ) 1
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
⊢ dist ((f ⋆[lsmul ℝ ℝ, μ] g) x₀) z₀ ≤ ε
have hif : Integrable f μ
Tactic: have hif : Integrable f μ := integrable_of_integral_eq_one hintf
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : CompleteSpace E'
f : G → ℝ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hf : support f ⊆ ball 0 R
hnf : ∀ (x : G), 0 ≤ f x
hintf : Eq (α := ℝ) (∫ (x : G), f x ∂μ) 1
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hif : Integrable f μ
⊢ dist ((f ⋆[lsmul ℝ ℝ, μ] g) x₀) z₀ ≤ ε
have h : z₀ = ∫ (t : G), (((lsmul ℝ ℝ : (a : ℝ) → E' →L[ℝ] E') (f t) : E' →L[ℝ] E') : (a : E') → E') z₀ ∂μ
Tactic: convert! (dist_convolution_le' (lsmul ℝ ℝ) hε hif hf hmg hg).trans _
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : CompleteSpace E'
f : G → ℝ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hf : support f ⊆ ball 0 R
hnf : ∀ (x : G), 0 ≤ f x
hintf : Eq (α := ℝ) (∫ (x : G), f x ∂μ) 1
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hif : Integrable f μ
h : z₀ = ∫ (t : G), (((lsmul ℝ ℝ : (a : ℝ) → E' →L[ℝ] E') (f t) : E' →L[ℝ] E') : (a : E') → E') z₀ ∂μ
⊢ dist ((f ⋆[lsmul ℝ ℝ, μ] g) x₀) z₀ ≤ ε
have convert_2 : (norm.{uE'} (E := ℝ →L[ℝ] E' →L[ℝ] E') (lsmul ℝ ℝ) * ∫ (x : G), ‖f x‖ ∂μ) * ε ≤ ε
Tactic: convert! (dist_convolution_le' (lsmul ℝ ℝ) hε hif hf hmg hg).trans _
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : CompleteSpace E'
f : G → ℝ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hf : support f ⊆ ball 0 R
hnf : ∀ (x : G), 0 ≤ f x
hintf : Eq (α := ℝ) (∫ (x : G), f x ∂μ) 1
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hif : Integrable f μ
⊢ z₀ = ∫ (t : G), (((lsmul ℝ ℝ : (a : ℝ) → E' →L[ℝ] E') (f t) : E' →L[ℝ] E') : (a : E') → E') z₀ ∂μ
have h : z₀ = ∫ (t : G), f t • z₀ ∂μ
Tactic: simp_rw [lsmul_apply, integral_smul_const, hintf, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : CompleteSpace E'
f : G → ℝ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hf : support f ⊆ ball 0 R
hnf : ∀ (x : G), 0 ≤ f x
hintf : Eq (α := ℝ) (∫ (x : G), f x ∂μ) 1
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hif : Integrable f μ
h : z₀ = ∫ (t : G), f t • z₀ ∂μ
⊢ z₀ = ∫ (t : G), (((lsmul ℝ ℝ : (a : ℝ) → E' →L[ℝ] E') (f t) : E' →L[ℝ] E') : (a : E') → E') z₀ ∂μ
have h₁ : z₀ = HSMul.hSMul (α := ℝ) (∫ (x : G), f x ∂μ) z₀
Tactic: simp_rw [lsmul_apply, integral_smul_const, hintf, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : CompleteSpace E'
f : G → ℝ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hf : support f ⊆ ball 0 R
hnf : ∀ (x : G), 0 ≤ f x
hintf : Eq (α := ℝ) (∫ (x : G), f x ∂μ) 1
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hif : Integrable f μ
h : z₀ = ∫ (t : G), f t • z₀ ∂μ
h₁ : z₀ = HSMul.hSMul (α := ℝ) (∫ (x : G), f x ∂μ) z₀
⊢ z₀ = ∫ (t : G), (((lsmul ℝ ℝ : (a : ℝ) → E' →L[ℝ] E') (f t) : E' →L[ℝ] E') : (a : E') → E') z₀ ∂μ
have h₂ : z₀ = HSMul.hSMul (α := ℝ) 1 z₀
Tactic: simp_rw [lsmul_apply, integral_smul_const, hintf, one_smul]