awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convolution
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 : AddGroup G
inst_9 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
s : Set G
hs : MeasurableSet s
h2s :
  (support.{uG, uF} (M := F) fun (t : G) ↦
      (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))) ⊆
    s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))
s' : Set G := (fun (t : G) ↦ -t + x₀) ⁻¹' s
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' s')
⊢ ∀ᵐ (t : G) ∂μ.restrict s,
    norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F) ≤
      s.indicator (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖) t

Tactic:
have : ∀ᵐ t : G ∂μ.restrict s,
      ‖L (f t) (g (x₀ - t))‖ ≤ s.indicator (fun t => ‖L‖ * ‖f t‖ * ⨆ i : s', ‖g i‖) t := by
    filter_upwards
    refine le_indicator (fun t ht => ?_) fun t ht => ?_
    · apply_rules [L.le_of_opNorm₂_le_of_le, le_rfl]
      refine (le_ciSup_set hbg <| mem_preimage.mpr ?_)
      rwa [neg_sub, sub_add_cancel]
    · have : t ∉ support fun t => L (f t) (g (x₀ - t)) := mt (fun h => h2s h) ht
      rw [notMem_support.mp this, norm_zero]
-- Module: Mathlib.Analysis.Convolution
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 : AddGroup G
inst_9 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
s : Set G
hs : MeasurableSet s
h2s :
  (support.{uG, uF} (M := F) fun (t : G) ↦
      (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))) ⊆
    s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))
s' : Set G := (fun (t : G) ↦ -t + x₀) ⁻¹' s
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' s')
this :
  ∀ᵐ (t : G) ∂μ.restrict s,
    norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F) ≤
      s.indicator (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖) t
⊢ IntegrableOn.{uG, uF} (ε := F)
    (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))) s μ

Tactic:
Integrable.mono' ?_ ?_ this

Premises used: MeasureTheory.Integrable.mono', MeasureTheory.IntegrableOn
-- Module: Mathlib.Analysis.Convolution
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 : AddGroup G
inst_9 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
s : Set G
hs : MeasurableSet s
h2s :
  (support.{uG, uF} (M := F) fun (t : G) ↦
      (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))) ⊆
    s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))
s' : Set G := (fun (t : G) ↦ -t + x₀) ⁻¹' s
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' s')
this :
  ∀ᵐ (t : G) ∂μ.restrict s,
    norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F) ≤
      s.indicator (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖) t
refine_1 :
  Integrable (ε := ℝ) (s.indicator fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖) (μ.restrict s)
refine_2 :
  AEStronglyMeasurable.{uG, uF} (β := F)
    (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))) (μ.restrict s)
⊢ IntegrableOn.{uG, uF} (ε := F)
    (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))) s μ

Tactic:
refine Integrable.mono' ?_ ?_ this

Premises used: MeasureTheory.Integrable.mono'
-- Module: Mathlib.Analysis.Convolution
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 : AddGroup G
inst_9 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
s : Set G
hs : MeasurableSet s
h2s :
  (support.{uG, uF} (M := F) fun (t : G) ↦
      (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))) ⊆
    s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))
s' : Set G := (fun (t : G) ↦ -t + x₀) ⁻¹' s
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' s')
this :
  ∀ᵐ (t : G) ∂μ.restrict s,
    norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F) ≤
      s.indicator (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖) t
refine_1 : IntegrableOn (ε := ℝ) (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖) s (μ.restrict s)
⊢ Integrable (ε := ℝ) (s.indicator fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖) (μ.restrict s)

Tactic:
rw [integrable_indicator_iff hs]

Premises used: MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.Analysis.Convolution
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 : AddGroup G
inst_9 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
s : Set G
hs : MeasurableSet s
h2s :
  (support.{uG, uF} (M := F) fun (t : G) ↦
      (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))) ⊆
    s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))
s' : Set G := (fun (t : G) ↦ -t + x₀) ⁻¹' s
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' s')
this :
  ∀ᵐ (t : G) ∂μ.restrict s,
    norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F) ≤
      s.indicator (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖) t
⊢ IntegrableOn (ε := ℝ) (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖) s (μ.restrict s)

Tactic:
((hf.norm.const_mul _).mul_const _).integrableOn

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.Integrable.mul_const, MeasureTheory.Integrable.integrableOn, MeasureTheory.Integrable.norm
-- Module: Mathlib.Analysis.Convolution
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 : AddGroup G
inst_9 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
s : Set G
hs : MeasurableSet s
h2s :
  (support.{uG, uF} (M := F) fun (t : G) ↦
      (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))) ⊆
    s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))
s' : Set G := (fun (t : G) ↦ -t + x₀) ⁻¹' s
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' s')
this :
  ∀ᵐ (t : G) ∂μ.restrict s,
    norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F) ≤
      s.indicator (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖) t
⊢ IntegrableOn (ε := ℝ) (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖) s (μ.restrict s)

Tactic:
exact ((hf.norm.const_mul _).mul_const _).integrableOn

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.Integrable.mul_const, MeasureTheory.Integrable.integrableOn, MeasureTheory.Integrable.norm
-- Module: Mathlib.Analysis.Convolution
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 : AddGroup G
inst_9 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
s : Set G
hs : MeasurableSet s
h2s :
  (support.{uG, uF} (M := F) fun (t : G) ↦
      (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))) ⊆
    s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))
s' : Set G := (fun (t : G) ↦ -t + x₀) ⁻¹' s
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' s')
this :
  ∀ᵐ (t : G) ∂μ.restrict s,
    norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F) ≤
      s.indicator (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖) t
⊢ AEStronglyMeasurable.{uG, uF} (β := F)
    (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))) (μ.restrict s)

Tactic:
hf.aestronglyMeasurable.convolution_integrand_snd' L hmg

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd'
-- Module: Mathlib.Analysis.Convolution
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 : AddGroup G
inst_9 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
s : Set G
hs : MeasurableSet s
h2s :
  (support.{uG, uF} (M := F) fun (t : G) ↦
      (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))) ⊆
    s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))
s' : Set G := (fun (t : G) ↦ -t + x₀) ⁻¹' s
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' s')
this :
  ∀ᵐ (t : G) ∂μ.restrict s,
    norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F) ≤
      s.indicator (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖) t
⊢ AEStronglyMeasurable.{uG, uF} (β := F)
    (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))) (μ.restrict s)

Tactic:
exact hf.aestronglyMeasurable.convolution_integrand_snd' L hmg

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd'
-- Module: Mathlib.Analysis.Convolution
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 : AddGroup G
inst_9 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
h : ConvolutionExistsAt (fun (x : G) ↦ ‖f x‖) (fun (x : G) ↦ ‖g x‖) x₀ (mul ℝ ℝ) μ
hmf : AEStronglyMeasurable f μ
hmg : AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) μ)
⊢ ConvolutionExistsAt f g x₀ L μ

Tactic:
(h.const_mul ‖L‖).mono'
    (hmf.convolution_integrand_snd' L hmg) (Eventually.of_forall fun x => ?_)

Premises used: Norm.norm, MeasureTheory.Integrable.const_mul, MeasureTheory.Integrable.mono', MeasureTheory.ConvolutionExistsAt, Filter.Eventually.of_forall, MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd'
-- Module: Mathlib.Analysis.Convolution
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 : AddGroup G
inst_9 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
h : ConvolutionExistsAt (fun (x : G) ↦ ‖f x‖) (fun (x : G) ↦ ‖g x‖) x₀ (mul ℝ ℝ) μ
hmf : AEStronglyMeasurable f μ
hmg : AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) μ)
refine :
  ∀ (x : G),
    norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f x) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - x)) : F) ≤
      HMul.hMul (β := ℝ) ‖L‖
        (((mul ℝ ℝ : (a : ℝ) → ℝ →L[ℝ] ℝ) ((fun (x : G) ↦ ‖f x‖) x) : (a : ℝ) → ℝ) ((fun (x : G) ↦ ‖g x‖) (x₀ - x)) : ℝ)
⊢ ConvolutionExistsAt f g x₀ L μ

Tactic:
refine (h.const_mul ‖L‖).mono'
    (hmf.convolution_integrand_snd' L hmg) (Eventually.of_forall fun x => ?_)

Premises used: Norm.norm, MeasureTheory.Integrable.const_mul, MeasureTheory.Integrable.mono', Filter.Eventually.of_forall, MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd'
-- Module: Mathlib.Analysis.Convolution
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 : AddGroup G
inst_9 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
h : ConvolutionExistsAt (fun (x : G) ↦ ‖f x‖) (fun (x : G) ↦ ‖g x‖) x₀ (mul ℝ ℝ) μ
hmf : AEStronglyMeasurable f μ
hmg : AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) μ)
x : G
rw :
  norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f x) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - x)) : F) ≤
    ‖L‖ * (fun (x : G) ↦ ‖f x‖) x * (fun (x : G) ↦ ‖g x‖) (x₀ - x)
⊢ norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f x) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - x)) : F) ≤
    HMul.hMul (β := ℝ) ‖L‖
      (((mul ℝ ℝ : (a : ℝ) → ℝ →L[ℝ] ℝ) ((fun (x : G) ↦ ‖f x‖) x) : (a : ℝ) → ℝ) ((fun (x : G) ↦ ‖g x‖) (x₀ - x)) : ℝ)

Tactic:
rw [mul_apply', ← mul_assoc]

Premises used: mul_assoc, ContinuousLinearMap.mul_apply'
-- Module: Mathlib.Analysis.Convolution
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 : AddGroup G
inst_9 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
h : ConvolutionExistsAt (fun (x : G) ↦ ‖f x‖) (fun (x : G) ↦ ‖g x‖) x₀ (mul ℝ ℝ) μ
hmf : AEStronglyMeasurable f μ
hmg : AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) μ)
x : G
⊢ norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f x) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - x)) : F) ≤
    ‖L‖ * (fun (x : G) ↦ ‖f x‖) x * (fun (x : G) ↦ ‖g x‖) (x₀ - x)

Tactic:
apply L.le_opNorm₂

Premises used: ContinuousLinearMap.le_opNorm₂
-- Module: Mathlib.Analysis.Convolution
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 : AddGroup G
inst_9 : MeasurableAdd₂ G
inst_10 : MeasurableNeg G
inst_11 : SFinite μ
inst_12 : μ.IsAddRightInvariant
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : G
⊢ AEStronglyMeasurable.{uG, uF} (β := F)
    (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t))) μ

Tactic:
hf.convolution_integrand_snd' L <|
    hg.mono_ac <| (quasiMeasurePreserving_sub_left_of_right_invariant μ x).absolutelyContinuous

Premises used: MeasureTheory.AEStronglyMeasurable.mono_ac, MeasureTheory.quasiMeasurePreserving_sub_left_of_right_invariant, MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd', MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous
-- Module: Mathlib.Analysis.Convolution
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 : AddGroup G
inst_9 : MeasurableAdd₂ G
inst_10 : MeasurableNeg G
inst_11 : SFinite μ
inst_12 : μ.IsAddRightInvariant
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : G
⊢ AEStronglyMeasurable.{uG, uF} (β := F)
    (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f (x - t)) : E' →L[𝕜] F) : (a : E') → F) (g t)) μ

Tactic:
(hf.mono_ac
        (quasiMeasurePreserving_sub_left_of_right_invariant μ
            x).absolutelyContinuous).convolution_integrand_swap_snd'
    L hg

Premises used: MeasureTheory.AEStronglyMeasurable.convolution_integrand_swap_snd', MeasureTheory.AEStronglyMeasurable.mono_ac, MeasureTheory.quasiMeasurePreserving_sub_left_of_right_invariant, MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous
-- Module: Mathlib.Analysis.Convolution
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 : AddGroup G
inst_9 : MeasurableAdd₂ G
inst_10 : MeasurableNeg G
inst_11 : SFinite μ
inst_12 : μ.IsAddRightInvariant
x₀ : G
h : ConvolutionExistsAt (fun (x : G) ↦ ‖f x‖) (fun (x : G) ↦ ‖g x‖) x₀ (mul ℝ ℝ) μ
hmf : AEStronglyMeasurable f μ
hmg : AEStronglyMeasurable g μ
⊢ ConvolutionExistsAt f g x₀ L μ

Tactic:
h.of_norm' L hmf <|
    hmg.mono_ac (quasiMeasurePreserving_sub_left_of_right_invariant μ x₀).absolutelyContinuous

Premises used: MeasureTheory.ConvolutionExistsAt.of_norm', MeasureTheory.AEStronglyMeasurable.mono_ac, MeasureTheory.quasiMeasurePreserving_sub_left_of_right_invariant, MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous
-- Module: Mathlib.Analysis.Convolution
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 : AddGroup G
inst_9 : MeasurableAdd₂ G
inst_10 : MeasurableNeg G
inst_11 : SFinite μ
inst_12 : μ.IsAddRightInvariant
inst_13 : SFinite ν
hf : AEStronglyMeasurable f ν
hg : AEStronglyMeasurable g μ
⊢ AEStronglyMeasurable.{uG, uF} (β := F)
    (fun (p : G × G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f p.2) : E' →L[𝕜] F) : (a : E') → F) (g (p.1 - p.2))) (μ.prod ν)

Tactic:
hf.convolution_integrand' L <|
    hg.mono_ac (quasiMeasurePreserving_sub_of_right_invariant μ ν).absolutelyContinuous

Premises used: MeasureTheory.AEStronglyMeasurable.mono_ac, MeasureTheory.quasiMeasurePreserving_sub_of_right_invariant, MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous, MeasureTheory.AEStronglyMeasurable.convolution_integrand'
-- Module: Mathlib.Analysis.Convolution
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 : AddGroup G
inst_9 : MeasurableAdd₂ G
inst_10 : MeasurableNeg G
inst_11 : SFinite μ
inst_12 : μ.IsAddRightInvariant
inst_13 : SFinite ν
hf : Integrable f ν
hg : Integrable g μ
⊢ AEStronglyMeasurable.{uG, uF} (β := F)
    (fun (p : G × G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f p.2) : E' →L[𝕜] F) : (a : E') → F) (g (p.1 - p.2))) (μ.prod ν)

Tactic:
have h_meas : AEStronglyMeasurable (fun p : G × G => L (f p.2) (g (p.1 - p.2))) (μ.prod ν) :=
    hf.aestronglyMeasurable.convolution_integrand L hg.aestronglyMeasurable
-- Module: Mathlib.Analysis.Convolution
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 : AddGroup G
inst_9 : MeasurableAdd₂ G
inst_10 : MeasurableNeg G
inst_11 : SFinite μ
inst_12 : μ.IsAddRightInvariant
inst_13 : SFinite ν
hf : Integrable f ν
hg : Integrable g μ
h_meas :
  AEStronglyMeasurable.{uG, uF} (β := F)
    (fun (p : G × G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f p.2) : E' →L[𝕜] F) : (a : E') → F) (g (p.1 - p.2))) (μ.prod ν)
⊢ AEStronglyMeasurable (β := ℝ)
    (fun (y : G) ↦
      ∫ (x : G),
        Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (g (x - y)) : F) ∂μ)
    ν

Tactic:
have h2_meas : AEStronglyMeasurable (fun y : G => ∫ x : G, ‖L (f y) (g (x - y))‖ ∂μ) ν :=
    h_meas.prod_swap.norm.integral_prod_right'
-- Module: Mathlib.Analysis.Convolution
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 : AddGroup G
inst_9 : MeasurableAdd₂ G
inst_10 : MeasurableNeg G
inst_11 : SFinite μ
inst_12 : μ.IsAddRightInvariant
inst_13 : SFinite ν
hf : Integrable f ν
hg : Integrable g μ
h_meas :
  AEStronglyMeasurable.{uG, uF} (β := F)
    (fun (p : G × G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f p.2) : E' →L[𝕜] F) : (a : E') → F) (g (p.1 - p.2))) (μ.prod ν)
h2_meas :
  AEStronglyMeasurable (β := ℝ)
    (fun (y : G) ↦
      ∫ (x : G),
        Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (g (x - y)) : F) ∂μ)
    ν
simp_rw :
  (∀ᵐ (y : G) ∂ν,
      Integrable.{uF, uG} (ε := F)
        (fun (x : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (g (x - y))) μ) ∧
    Integrable (ε := ℝ)
      (fun (y : G) ↦
        ∫ (x : G),
          Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (g (x - y)) : F) ∂μ)
      ν
⊢ Integrable.{uF, uG} (ε := F)
    (fun (p : G × G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f p.2) : E' →L[𝕜] F) : (a : E') → F) (g (p.1 - p.2))) (μ.prod ν)

Tactic:
simp_rw [integrable_prod_iff' h_meas]

Premises used: MeasureTheory.integrable_prod_iff'