awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : AddGroup G
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup G
inst_11 : BorelSpace G
hcf : HasCompactSupport f
hf : LocallyIntegrable f μ
hg : Continuous[inst_9, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ : G
⊢ (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))) ⊆
    support f
have refine : ∀ (t : G) (ht : f t = 0),
  Eq.{uF + 1} (α := F)
    ((fun (t : G) ↦ ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)) t) 0
Tactic: refine fun t => mt fun ht : f t = 0 => ?_
-- 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 : AddGroup G
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup G
inst_11 : BorelSpace G
hcf : HasCompactSupport f
hf : LocallyIntegrable f μ
hg : Continuous[inst_9, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ t : G
ht : f t = 0
simp_rw simp_rw₁ :
  Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F) (0 : F)
⊢ Eq.{uF + 1} (α := F)
    ((fun (t : G) ↦ ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)) t) 0
have simp_rw₂ : Eq.{uF + 1} (α := F) (((L : (a : E) → E' →L[𝕜] F) 0 : (a : E') → F) (g (x₀ - t)) : F) (0 : F)
Tactic: simp_rw [ht, L.map_zero₂]
-- 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 : AddCommGroup G
inst_9 : MeasurableNeg G
inst_10 : μ.IsAddLeftInvariant
inst_11 : MeasurableAdd₂ G
inst_12 : SFinite μ
x₀ : G
s : Set G
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' (fun (t : G) ↦ x₀ - t) ⁻¹' s)
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 g μ
⊢ ConvolutionExistsAt f g x₀ L μ
have refine_1 : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' (fun (t : G) ↦ -t + x₀) ⁻¹' s)
Tactic: refine BddAbove.convolutionExistsAt' L ?_ hs h2s hf ?_
-- 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 : AddCommGroup G
inst_9 : MeasurableNeg G
inst_10 : μ.IsAddLeftInvariant
inst_11 : MeasurableAdd₂ G
inst_12 : SFinite μ
x₀ : G
s : Set G
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' (fun (t : G) ↦ x₀ - t) ⁻¹' s)
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 g μ
refine_1 : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' (fun (t : G) ↦ -t + x₀) ⁻¹' s)
⊢ ConvolutionExistsAt f g x₀ L μ
have refine_2 : AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))
Tactic: refine BddAbove.convolutionExistsAt' L ?_ hs h2s hf ?_
-- 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 : AddCommGroup G
inst_9 : MeasurableNeg G
inst_10 : μ.IsAddLeftInvariant
inst_11 : MeasurableAdd₂ G
inst_12 : SFinite μ
x₀ : G
s : Set G
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' (fun (t : G) ↦ x₀ - t) ⁻¹' s)
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 g μ
⊢ AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))
have this : AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) μ)
Tactic: have : AEStronglyMeasurable g (map (fun t : G => x₀ - t) μ) :=
      hmg.mono_ac (quasiMeasurePreserving_sub_left_of_right_invariant μ x₀).absolutelyContinuous
-- 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 : AddCommGroup G
inst_9 : MeasurableNeg G
inst_10 : μ.IsAddLeftInvariant
inst_11 : MeasurableAdd₂ G
inst_12 : SFinite μ
x₀ : G
s : Set G
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' (fun (t : G) ↦ x₀ - t) ⁻¹' s)
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 g μ
this : AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) μ)
⊢ AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))
have refine_2 : LE.le (α := Measure G) (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s)) (Measure.map (fun (t : G) ↦ x₀ - t) μ)
Tactic: apply this.mono_measure
-- 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'
x : G
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 : AddCommGroup G
inst_9 : MeasurableNeg G
inst_10 : μ.IsAddLeftInvariant
inst_11 : MeasurableAdd G
inst_12 : μ.IsNegInvariant
⊢ ConvolutionExistsAt g f x L.flip μ ↔ ConvolutionExistsAt f g x L μ
have simp_rw : Integrable.{uF, uG} (ε := F)
    (fun (t : G) ↦ (((L.flip : (a : E') → E →L[𝕜] F) (g t) : E →L[𝕜] F) : (a : E) → F) (f (x - t))) μ ↔
  Integrable.{uF, uG} (ε := F)
    (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t))) μ
Tactic: simp_rw [ConvolutionExistsAt, ← integrable_comp_sub_left (fun t => L (f t) (g (x - t))) x,
    sub_sub_cancel, flip_apply]
-- 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'
x : G
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 : AddCommGroup G
inst_9 : MeasurableNeg G
inst_10 : μ.IsAddLeftInvariant
inst_11 : MeasurableAdd G
inst_12 : μ.IsNegInvariant
simp_rw :
  Integrable.{uF, uG} (ε := F)
      (fun (t : G) ↦ (((L.flip : (a : E') → E →L[𝕜] F) (g t) : E →L[𝕜] F) : (a : E) → F) (f (x - t))) μ ↔
    Integrable.{uF, uG} (ε := F)
      (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t))) μ
⊢ ConvolutionExistsAt g f x L.flip μ ↔ ConvolutionExistsAt f g x L μ
have simp_rw₁ : Integrable.{uF, uG} (ε := F)
    (fun (t : G) ↦ (((L.flip : (a : E') → E →L[𝕜] F) (g t) : E →L[𝕜] F) : (a : E) → F) (f (x - t))) μ ↔
  Integrable.{uF, uG} (ε := F)
    (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f (x - t)) : E' →L[𝕜] F) : (a : E') → F) (g (x - (x - t)))) μ
Tactic: simp_rw [ConvolutionExistsAt, ← integrable_comp_sub_left (fun t => L (f t) (g (x - t))) x,
    sub_sub_cancel, flip_apply]
-- 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'
x : G
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 : AddCommGroup G
inst_9 : MeasurableNeg G
inst_10 : μ.IsAddLeftInvariant
inst_11 : MeasurableAdd G
inst_12 : μ.IsNegInvariant
simp_rw :
  Integrable.{uF, uG} (ε := F)
      (fun (t : G) ↦ (((L.flip : (a : E') → E →L[𝕜] F) (g t) : E →L[𝕜] F) : (a : E) → F) (f (x - t))) μ ↔
    Integrable.{uF, uG} (ε := F)
      (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t))) μ
simp_rw₁ :
  Integrable.{uF, uG} (ε := F)
      (fun (t : G) ↦ (((L.flip : (a : E') → E →L[𝕜] F) (g t) : E →L[𝕜] F) : (a : E) → F) (f (x - t))) μ ↔
    Integrable.{uF, uG} (ε := F)
      (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f (x - t)) : E' →L[𝕜] F) : (a : E') → F) (g (x - (x - t)))) μ
⊢ ConvolutionExistsAt g f x L.flip μ ↔ ConvolutionExistsAt f g x L μ
have simp_rw₂ : Integrable.{uF, uG} (ε := F)
    (fun (t : G) ↦ (((L.flip : (a : E') → E →L[𝕜] F) (g t) : E →L[𝕜] F) : (a : E) → F) (f (x - t))) μ ↔
  Integrable.{uF, uG} (ε := F)
    (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f (x - t)) : E' →L[𝕜] F) : (a : E') → F) (g t)) μ
Tactic: simp_rw [ConvolutionExistsAt, ← integrable_comp_sub_left (fun t => L (f t) (g (x - t))) x,
    sub_sub_cancel, flip_apply]
-- 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'
x : G
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 : AddCommGroup G
inst_9 : MeasurableNeg G
inst_10 : μ.IsAddLeftInvariant
inst_11 : MeasurableAdd G
inst_12 : μ.IsNegInvariant
h : ConvolutionExistsAt f g x L μ
⊢ Integrable.{uF, uG} (ε := F)
    (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f (x - t)) : E' →L[𝕜] F) : (a : E') → F) (g t)) μ
have h₁ : ∀ (x_1 : G), x_1 = x - (x - x_1)
Tactic: convert! h.comp_sub_left x
-- 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 : AddGroup G
inst_10 : SMulCommClass ℝ 𝕜 F
y : 𝕜
⊢ y • f ⋆[L, μ] g = y • (f ⋆[L, μ] g)
have h : ∀ (x : G), (y • f ⋆[L, μ] g) x = (y • (f ⋆[L, μ] g)) x
Tactic: ext
-- 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 : AddGroup G
inst_10 : SMulCommClass ℝ 𝕜 F
y : 𝕜
⊢ f ⋆[L, μ] y • g = y • (f ⋆[L, μ] g)
have h : ∀ (x : G), (f ⋆[L, μ] y • g) x = (y • (f ⋆[L, μ] g)) x
Tactic: ext
-- 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
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 : AddGroup G
⊢ 0 ⋆[L, μ] g = 0
have h : ∀ (x : G), (0 ⋆[L, μ] g) x = 0 x
Tactic: ext
-- 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
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 : AddGroup G
x : G
⊢ (0 ⋆[L, μ] g) x = 0 x
have h : Eq.{uF + 1} (α := F) (∫ (t : G), ((L : (a : E) → E' →L[𝕜] F) (0 t) : (a : E') → F) (g (x - t)) ∂μ) (0 x)
Tactic: simp_rw [convolution_def, Pi.zero_apply, L.map_zero₂, integral_zero]
-- 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
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 : AddGroup G
x : G
h : Eq.{uF + 1} (α := F) (∫ (t : G), ((L : (a : E) → E' →L[𝕜] F) (0 t) : (a : E') → F) (g (x - t)) ∂μ) (0 x)
⊢ (0 ⋆[L, μ] g) x = 0 x
have h₁ : Eq.{uF + 1} (α := F) (∫ (t : G), ((L : (a : E) → E' →L[𝕜] F) 0 : (a : E') → F) (g (x - t)) ∂μ) 0
Tactic: simp_rw [convolution_def, Pi.zero_apply, L.map_zero₂, integral_zero]
-- 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
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 : AddGroup G
x : G
h : Eq.{uF + 1} (α := F) (∫ (t : G), ((L : (a : E) → E' →L[𝕜] F) (0 t) : (a : E') → F) (g (x - t)) ∂μ) (0 x)
h₁ : Eq.{uF + 1} (α := F) (∫ (t : G), ((L : (a : E) → E' →L[𝕜] F) 0 : (a : E') → F) (g (x - t)) ∂μ) 0
⊢ (0 ⋆[L, μ] g) x = 0 x
have h₂ : Eq.{uF + 1} (α := F) (∫ (t : G), 0 ∂μ) 0
Tactic: simp_rw [convolution_def, Pi.zero_apply, L.map_zero₂, integral_zero]
-- 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
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 : AddGroup G
⊢ f ⋆[L, μ] 0 = 0
have h : ∀ (x : G), (f ⋆[L, μ] 0) x = 0 x
Tactic: ext
-- 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
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 : AddGroup G
x : G
⊢ (f ⋆[L, μ] 0) x = 0 x
have h : Eq.{uF + 1} (α := F) (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (0 (x - t)) ∂μ) (0 x)
Tactic: simp_rw [convolution_def, Pi.zero_apply, (L _).map_zero, integral_zero]
-- 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
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 : AddGroup G
x : G
h :
  Eq.{uF + 1} (α := F) (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (0 (x - t)) ∂μ)
    (0 x)
⊢ (f ⋆[L, μ] 0) x = 0 x
have h₁ : Eq.{uF + 1} (α := F) (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) 0 ∂μ) 0
Tactic: simp_rw [convolution_def, Pi.zero_apply, (L _).map_zero, integral_zero]
-- 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
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 : AddGroup G
x : G
h :
  Eq.{uF + 1} (α := F) (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (0 (x - t)) ∂μ)
    (0 x)
h₁ : Eq.{uF + 1} (α := F) (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) 0 ∂μ) 0
⊢ (f ⋆[L, μ] 0) x = 0 x
have h₂ : Eq.{uF + 1} (α := F) (∫ (t : G), 0 ∂μ) 0
Tactic: simp_rw [convolution_def, Pi.zero_apply, (L _).map_zero, integral_zero]
-- 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' : 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 : AddGroup G
hfg : ConvolutionExists f g L μ
hfg' : ConvolutionExists f g' L μ
⊢ f ⋆[L, μ] (g + g') = f ⋆[L, μ] g + f ⋆[L, μ] g'
have h : ∀ (x : G), (f ⋆[L, μ] (g + g')) x = (f ⋆[L, μ] g + f ⋆[L, μ] g') x
Tactic: ext x
-- 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 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 : AddGroup G
hfg : ConvolutionExists f g L μ
hfg' : ConvolutionExists f' g L μ
⊢ (f + f') ⋆[L, μ] g = f ⋆[L, μ] g + f' ⋆[L, μ] g
have h : ∀ (x : G), ((f + f') ⋆[L, μ] g) x = (f ⋆[L, μ] g + f' ⋆[L, μ] g) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
G : Type uG
x : G
inst : MeasurableSpace G
μ : Measure G
inst_1 : AddGroup G
f g g' : G → ℝ
hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x
have apply : LE.le.{uG} (α := G → ℝ)
  (fun (t : G) ↦ (((lsmul ℝ ℝ : (a : ℝ) → ℝ →L[ℝ] ℝ) (f t) : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) (g (x - t))) fun (t : G) ↦
  (((lsmul ℝ ℝ : (a : ℝ) → ℝ →L[ℝ] ℝ) (f t) : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) (g' (x - t))
Tactic: apply integral_mono hfg hfg'
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
G : Type uG
x : G
inst : MeasurableSpace G
μ : Measure G
inst_1 : AddGroup G
f g g' : G → ℝ
hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
t : G
⊢ f t * g (x - t) ≤ f t * g' (x - t)
have ha : 0 ≤ f t
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
G : Type uG
x : G
inst : MeasurableSpace G
μ : Measure G
inst_1 : AddGroup G
f g g' : G → ℝ
hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
t : G
ha : 0 ≤ f t
⊢ f t * g (x - t) ≤ f t * g' (x - t)
have hbc : g (x - t) ≤ g' (x - t)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
G : Type uG
x : G
inst : MeasurableSpace G
μ : Measure G
inst_1 : AddGroup G
f g g' : G → ℝ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
hg' : ∀ (x : G), 0 ≤ g' x
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x
have pos : ∀ (H : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ), (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x
Tactic: by_cases H : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
G : Type uG
x : G
inst : MeasurableSpace G
μ : Measure G
inst_1 : AddGroup G
f g g' : G → ℝ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
hg' : ∀ (x : G), 0 ≤ g' x
pos : ∀ (H : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ), (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x
have neg : ∀ (H : ¬ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ), (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x
Tactic: by_cases H : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
-- Lean 4 proof step from Mathlib.Analysis.Convolution (hypothesis)
Goal:
G : Type uG
x : G
inst : MeasurableSpace G
μ : Measure G
inst_1 : AddGroup G
f g g' : G → ℝ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
hg' : ∀ (x : G), 0 ≤ g' x
H : ¬ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x
have this : (f ⋆[lsmul ℝ ℝ, μ] g) x = 0
Tactic: have : (f ⋆[lsmul ℝ ℝ, μ] g) x = 0 := integral_undef H
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
G : Type uG
x : G
inst : MeasurableSpace G
μ : Measure G
inst_1 : AddGroup G
f g g' : G → ℝ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
hg' : ∀ (x : G), 0 ≤ g' x
H : ¬ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
this : (f ⋆[lsmul ℝ ℝ, μ] g) x = 0
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x
have neg : 0 ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x
Tactic: rw [this]
-- 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 f' : G → E
g 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 : AddGroup G
inst_10 : MeasurableAdd₂ G
inst_11 : MeasurableNeg G
inst_12 : SFinite μ
inst_13 : μ.IsAddRightInvariant
h1 : f =ᶠ[ae μ] f'
h2 : g =ᶠ[ae μ] g'
⊢ f ⋆[L, μ] g = f' ⋆[L, μ] g'
have h : ∀ (x : G), (f ⋆[L, μ] g) x = (f' ⋆[L, μ] g') x
Tactic: ext x