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
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) ∂μ)
    ν
⊢ (∀ᵐ (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) ∂μ)
      ν

Tactic:
⟨Eventually.of_forall fun t => (L (f t)).integrable_comp (hg.comp_sub_right t), ?_⟩

Premises used: Filter.Eventually.of_forall, ContinuousLinearMap.integrable_comp, And.intro, DFunLike.coe, MeasureTheory.Integrable.comp_sub_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) ∂μ)
    ν
refine :
  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) ∂μ)
    ν
⊢ (∀ᵐ (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) ∂μ)
      ν

Tactic:
refine ⟨Eventually.of_forall fun t => (L (f t)).integrable_comp (hg.comp_sub_right t), ?_⟩
-- 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) ∂μ)
    ν
⊢ 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) ∂μ)
    ν

Tactic:
Integrable.mono' ?_ h2_meas
      (Eventually.of_forall fun t => (?_ : _ ≤ ‖L‖ * ‖f t‖ * ∫ x, ‖g (x - t)‖ ∂μ))

Premises used: MeasureTheory.Integrable.mono', Filter.Eventually.of_forall
-- 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) ∂μ)
    ν
refine_1 : Integrable (ε := ℝ) (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ∫ (x : G), ‖g (x - t)‖ ∂μ) ν
refine_2 :
  ∀ (t : G),
    Norm.norm (E := ℝ)
        (∫ (x : G),
          Norm.norm.{uF} (E := F)
            ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ∂μ) ≤
      ‖L‖ * ‖f t‖ * ∫ (x : G), ‖g (x - t)‖ ∂μ
⊢ 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) ∂μ)
    ν

Tactic:
refine Integrable.mono' ?_ h2_meas
      (Eventually.of_forall fun t => (?_ : _ ≤ ‖L‖ * ‖f t‖ * ∫ x, ‖g (x - t)‖ ∂μ))

Premises used: MeasureTheory.Integrable.mono', Filter.Eventually.of_forall
-- 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) ∂μ)
    ν
refine_1 : Integrable (ε := ℝ) (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ∫ (x : G), ‖g x‖ ∂μ) ν
⊢ Integrable (ε := ℝ) (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ∫ (x : G), ‖g (x - t)‖ ∂μ) ν

Tactic:
simp only [integral_sub_right_eq_self (‖g ·‖)]

Premises used: Norm.norm, MeasureTheory.integral_sub_right_eq_self
-- 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) ∂μ)
    ν
⊢ Integrable (ε := ℝ) (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ∫ (x : G), ‖g x‖ ∂μ) ν

Tactic:
fun_prop
-- 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) ∂μ)
    ν
t : G
refine_2 :
  Norm.norm (E := ℝ)
      (∫ (x : G),
        Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ∂μ) ≤
    ∫ (a : G), ‖L‖ * ‖f t‖ * ‖g (a - t)‖ ∂μ
⊢ Norm.norm (E := ℝ)
      (∫ (x : G),
        Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ∂μ) ≤
    ‖L‖ * ‖f t‖ * ∫ (x : G), ‖g (x - t)‖ ∂μ

Tactic:
simp_rw [← integral_const_mul]

Premises used: MeasureTheory.integral_const_mul
-- 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) ∂μ)
    ν
t : G
⊢ LE.le (α := ℝ) 0
    (∫ (x : G),
      Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ∂μ)

Tactic:
positivity
-- 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) ∂μ)
    ν
t : G
refine_2 :
  LE.le (α := ℝ)
    (∫ (x : G),
      Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ∂μ)
    (∫ (a : G), ‖L‖ * ‖f t‖ * ‖g (a - t)‖ ∂μ)
⊢ Norm.norm (E := ℝ)
      (∫ (x : G),
        Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ∂μ) ≤
    ∫ (a : G), ‖L‖ * ‖f t‖ * ‖g (a - t)‖ ∂μ

Tactic:
rw [Real.norm_of_nonneg (by positivity)]

Premises used: Real.norm_of_nonneg
-- 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) ∂μ)
    ν
t : G
⊢ LE.le (α := ℝ)
    (∫ (x : G),
      Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ∂μ)
    (∫ (a : G), ‖L‖ * ‖f t‖ * ‖g (a - t)‖ ∂μ)

Tactic:
integral_mono_of_nonneg (Eventually.of_forall fun t => norm_nonneg _)
      ((hg.comp_sub_right t).norm.const_mul _) (Eventually.of_forall fun t => L.le_opNorm₂ _ _)

Premises used: MeasureTheory.Integrable.const_mul, HSub.hSub, Filter.Eventually.of_forall, ContinuousLinearMap.le_opNorm₂, MeasureTheory.integral_mono_of_nonneg, MeasureTheory.Integrable.norm, DFunLike.coe, norm_nonneg, MeasureTheory.Integrable.comp_sub_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) ∂μ)
    ν
t : G
⊢ LE.le (α := ℝ)
    (∫ (x : G),
      Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ∂μ)
    (∫ (a : G), ‖L‖ * ‖f t‖ * ‖g (a - t)‖ ∂μ)

Tactic:
exact integral_mono_of_nonneg (Eventually.of_forall fun t => norm_nonneg _)
      ((hg.comp_sub_right t).norm.const_mul _) (Eventually.of_forall fun t => L.le_opNorm₂ _ _)

Premises used: MeasureTheory.Integrable.const_mul, HSub.hSub, Filter.Eventually.of_forall, ContinuousLinearMap.le_opNorm₂, MeasureTheory.integral_mono_of_nonneg, MeasureTheory.Integrable.norm, norm_nonneg, MeasureTheory.Integrable.comp_sub_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 μ
⊢ ∀ᵐ (x : G) ∂μ, ConvolutionExistsAt f g x L ν

Tactic:
((integrable_prod_iff <|
          hf.aestronglyMeasurable.convolution_integrand L hg.aestronglyMeasurable).mp <|
      hf.convolution_integrand L hg).1

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.ConvolutionExistsAt, MeasureTheory.integrable_prod_iff, MeasureTheory.Integrable.convolution_integrand, And.left, Iff.mp, 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 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup G
inst_11 : BorelSpace G
x₀ : G
h :
  HasCompactSupport.{uG, uF} (β := F) fun (t : G) ↦
    (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))
hf : LocallyIntegrable f μ
hg : Continuous[inst_9, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
u : G ≃ₜ G := Homeomorph.trans (Homeomorph.neg G) (Homeomorph.addRight x₀)
v : G ≃ₜ G := Homeomorph.trans (Homeomorph.neg G) (Homeomorph.addLeft x₀)
apply :
  AEStronglyMeasurable (m₀ := inst_7) g
    (Measure.map (fun (t : G) ↦ (↑((toAddUnits : (a : G) → AddUnits G) x₀) : G) - t)
      (μ.restrict
        (tsupport.{uG, uF} (α := F) fun (t : G) ↦
          (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)))))
⊢ ConvolutionExistsAt f g x₀ L μ

Tactic:
apply ((u.isCompact_preimage.mpr h).bddAbove_image hg.norm.continuousOn).convolutionExistsAt' L
    isClosed_closure.measurableSet subset_closure (hf.integrableOn_isCompact h)

Premises used: Iff.mpr, Continuous.continuousOn, BddAbove.convolutionExistsAt', subset_closure, Homeomorph.isCompact_preimage, IsClosed.measurableSet, Continuous.norm, IsCompact.bddAbove_image, MeasureTheory.LocallyIntegrable.integrableOn_isCompact, isClosed_closure
-- 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 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup G
inst_11 : BorelSpace G
x₀ : G
h :
  HasCompactSupport.{uG, uF} (β := F) fun (t : G) ↦
    (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))
hf : LocallyIntegrable f μ
hg : Continuous[inst_9, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
u : G ≃ₜ G := Homeomorph.trans (Homeomorph.neg G) (Homeomorph.addRight x₀)
v : G ≃ₜ G := Homeomorph.trans (Homeomorph.neg G) (Homeomorph.addLeft x₀)
apply :
  MeasurableSet.{uG} (α := G)
    (tsupport.{uG, uF} (α := F) fun (t : G) ↦
      (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)))
⊢ AEStronglyMeasurable (g ∘ (⇑v : (a : G) → G))
    (μ.restrict
      (tsupport.{uG, uF} (α := F) fun (t : G) ↦
        (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))))

Tactic:
apply (hg.comp v.continuous).continuousOn.aestronglyMeasurable_of_isCompact h

Premises used: ContinuousOn.aestronglyMeasurable_of_isCompact, Continuous.continuousOn, Homeomorph.continuous, Continuous.comp
-- 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 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup G
inst_11 : BorelSpace G
x₀ : G
h :
  HasCompactSupport.{uG, uF} (β := F) fun (t : G) ↦
    (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))
hf : LocallyIntegrable f μ
hg : Continuous[inst_9, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
u : G ≃ₜ G := Homeomorph.trans (Homeomorph.neg G) (Homeomorph.addRight x₀)
v : G ≃ₜ G := Homeomorph.trans (Homeomorph.neg G) (Homeomorph.addLeft x₀)
⊢ MeasurableSet.{uG} (α := G)
    (tsupport.{uG, uF} (α := F) fun (t : G) ↦
      (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)))

Tactic:
(isClosed_tsupport _).measurableSet

Premises used: IsClosed.measurableSet, isClosed_tsupport
-- 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 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup G
inst_11 : BorelSpace G
x₀ : G
h :
  HasCompactSupport.{uG, uF} (β := F) fun (t : G) ↦
    (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))
hf : LocallyIntegrable f μ
hg : Continuous[inst_9, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
u : G ≃ₜ G := Homeomorph.trans (Homeomorph.neg G) (Homeomorph.addRight x₀)
v : G ≃ₜ G := Homeomorph.trans (Homeomorph.neg G) (Homeomorph.addLeft x₀)
⊢ MeasurableSet.{uG} (α := G)
    (tsupport.{uG, uF} (α := F) fun (t : G) ↦
      (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)))

Tactic:
exact (isClosed_tsupport _).measurableSet

Premises used: IsClosed.measurableSet, isClosed_tsupport
-- 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 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup G
inst_11 : BorelSpace G
x₀ : G
h :
  HasCompactSupport.{uG, uF} (β := F) fun (t : G) ↦
    (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))
hf : LocallyIntegrable f μ
hg : Continuous[inst_9, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
u : G ≃ₜ G := Homeomorph.trans (Homeomorph.neg G) (Homeomorph.addRight x₀)
v : G ≃ₜ G := Homeomorph.trans (Homeomorph.neg G) (Homeomorph.addLeft x₀)
⊢ AEStronglyMeasurable (g ∘ (⇑v : (a : G) → G))
    (μ.restrict
      (tsupport.{uG, uF} (α := F) fun (t : G) ↦
        (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))))

Tactic:
have A : AEStronglyMeasurable (g ∘ v)
      (μ.restrict (tsupport fun t : G => L (f t) (g (x₀ - t)))) := by
    apply (hg.comp v.continuous).continuousOn.aestronglyMeasurable_of_isCompact h
    exact (isClosed_tsupport _).measurableSet