awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h_1 : Membership.mem (γ := Set ℝ) (Ioi 0) x
t : ℝ
h : 0 < t
h' : t < x
⊢ t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t

Tactic:
Or.inr (Or.inl ⟨h, h'⟩)

Premises used: And.intro, Or.inl, Or.inr
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h_1 : Membership.mem (γ := Set ℝ) (Ioi 0) x
t : ℝ
h : 0 < t
h' : x ≤ t
⊢ t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t

Tactic:
Or.inr (Or.inr h')

Premises used: Or.inr
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h_1 : Membership.mem (γ := Set ℝ) (Ioi 0) x
t : ℝ
h : 0 < t
h' : t < x
⊢ t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t

Tactic:
exacts [Or.inr (Or.inl ⟨h, h'⟩), Or.inr (Or.inr h')]

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) x
t : ℝ
⊢ t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t

Tactic:
have : t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t := by
      rcases le_or_gt t 0 with (h | h)
      · exact Or.inl h
      · rcases lt_or_ge t x with (h' | h')
        exacts [Or.inr (Or.inl ⟨h, h'⟩), Or.inr (Or.inr h')]
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) x
t : ℝ
this : t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t
pos :
  ∀ (ht : t ≤ 0),
    Eq.{uF + 1} (α := F)
      ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
          t :
        F)
      ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F)
          (indicator (Ioi 0) g (x - t)) :
        F)
pos₁ :
  ∀ (ht : t ∈ Ioo 0 x),
    Eq.{uF + 1} (α := F)
      ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
          t :
        F)
      ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F)
          (indicator (Ioi 0) g (x - t)) :
        F)
pos₂ :
  ∀ (ht : x ≤ t),
    Eq.{uF + 1} (α := F)
      ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
          t :
        F)
      ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F)
          (indicator (Ioi 0) g (x - t)) :
        F)
⊢ Eq.{uF + 1} (α := F)
    ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
        t :
      F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)

Tactic:
rcases this with (ht | ht | ht)
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) x
t : ℝ
ht : t ≤ 0
pos :
  Eq.{uF + 1} (α := F) (0 : F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
pos₁ : Eq.{uF + 1} (α := F) (0 : F) (((L : (a : E) → E' →L[ℝ] F) 0 : (a : E') → F) (indicator (Ioi 0) g (x - t)) : F)
pos₂ : Eq.{uF + 1} (α := F) (0 : F) ((0 : (a : E') → F) (indicator (Ioi 0) g (x - t)) : F)
pos₃ pos₄ : Eq.{uF + 1} (α := F) 0 0
⊢ Eq.{uF + 1} (α := F)
    ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
        t :
      F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)

Tactic:
rw [indicator_of_notMem (notMem_Ioo_of_le ht), indicator_of_notMem (notMem_Ioi.mpr ht),
        map_zero, ContinuousLinearMap.zero_apply]

Premises used: Iff.mpr, Set.notMem_Ioi, map_zero, Set.indicator_of_notMem, Set.notMem_Ioo_of_le, ContinuousLinearMap.zero_apply
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) x
t : ℝ
ht : t ∈ Ioo 0 x
pos :
  Eq.{uF + 1} (α := 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) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
pos₁ :
  Eq.{uF + 1} (α := 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) (indicator (Ioi 0) g (x - t)) : F)
pos₂ pos₃ :
  Eq.{uF + 1} (α := 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) (g (x - t)) : F)
⊢ Eq.{uF + 1} (α := F)
    ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
        t :
      F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)

Tactic:
rw [indicator_of_mem ht, indicator_of_mem (mem_Ioi.mpr ht.1),
          indicator_of_mem (mem_Ioi.mpr <| sub_pos.mpr ht.2)]

Premises used: Iff.mpr, sub_pos, Set.mem_Ioi, Set.indicator_of_mem, And.right, And.left
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) x
t : ℝ
ht : x ≤ t
pos :
  Eq.{uF + 1} (α := F) (0 : F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
pos₁ :
  Eq.{uF + 1} (α := F) (0 : F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) 0 : F)
pos₂ pos₃ : Eq.{uF + 1} (α := F) 0 0
⊢ Eq.{uF + 1} (α := F)
    ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
        t :
      F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)

Tactic:
rw [indicator_of_notMem (notMem_Ioo_of_ge ht),
          indicator_of_notMem (notMem_Ioi.mpr (sub_nonpos_of_le ht)), map_zero]

Premises used: Iff.mpr, Set.notMem_Ioi, map_zero, Set.notMem_Ioo_of_ge, sub_nonpos_of_le, Set.indicator_of_notMem
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : x ∉ Ioi 0
⊢ Eq.{uF + 1} (α := F) 0 (∫ (x : ℝ), 0 ∂ν)

Tactic:
(integral_zero ℝ F).symm

Premises used: Real, Eq.symm, MeasureTheory.integral_zero
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : x ∉ Ioi 0
h₁ :
  ∀ (t : ℝ),
    Eq.{uF + 1} (α := F)
      ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F)
          (indicator (Ioi 0) g (x - t)) :
        F)
      (0 : F)
⊢ Eq.{uF + 1} (α := F) 0
    (∫ (t : ℝ),
      (((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F)
        (indicator (Ioi 0) g (x - t)) ∂ν)

Tactic:
convert! (integral_zero ℝ F).symm with t

Premises used: Real, Eq.symm, MeasureTheory.integral_zero
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : x ∉ Ioi 0
t : ℝ
pos :
  ∀ (ht : 0 < t),
    Eq.{uF + 1} (α := F)
      ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F)
          (indicator (Ioi 0) g (x - t)) :
        F)
      (0 : F)
neg :
  ∀ (ht : ¬0 < t),
    Eq.{uF + 1} (α := F)
      ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F)
          (indicator (Ioi 0) g (x - t)) :
        F)
      (0 : F)
⊢ Eq.{uF + 1} (α := F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
    (0 : F)

Tactic:
by_cases ht : 0 < t
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : x ∉ Ioi 0
t : ℝ
ht : 0 < t
rw : x - t ∉ Ioi 0
⊢ Eq.{uF + 1} (α := F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
    (0 : F)

Tactic:
rw [indicator_of_notMem (_ : x - t ∉ Ioi 0), map_zero]

Premises used: map_zero, Set.indicator_of_notMem
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : x ∉ Ioi 0
t : ℝ
ht : 0 < t
rw : ∀ (h : x ≤ 0) (t : ℝ) (ht : 0 < t), x - t ≤ 0
⊢ x - t ∉ Ioi 0

Tactic:
rw [notMem_Ioi] at h ⊢

Premises used: Set.notMem_Ioi
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : x ≤ 0
t : ℝ
ht : 0 < t
⊢ x - t ≤ 0

Tactic:
sub_nonpos.mpr (h.trans ht.le)

Premises used: Iff.mpr, LT.lt.le, LE.le.trans, sub_nonpos
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : x ≤ 0
t : ℝ
ht : 0 < t
⊢ x - t ≤ 0

Tactic:
exact sub_nonpos.mpr (h.trans ht.le)

Premises used: Iff.mpr, LT.lt.le, LE.le.trans, sub_nonpos
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : x ∉ Ioi 0
t : ℝ
ht : ¬0 < t
neg : Eq.{uF + 1} (α := F) (((L : (a : E) → E' →L[ℝ] F) 0 : (a : E') → F) (indicator (Ioi 0) g (x - t)) : F) (0 : F)
neg₁ : Eq.{uF + 1} (α := F) ((0 : (a : E') → F) (indicator (Ioi 0) g (x - t)) : F) (0 : F)
neg₂ neg₃ : Eq.{uF + 1} (α := F) 0 0
⊢ Eq.{uF + 1} (α := F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
    (0 : F)

Tactic:
rw [indicator_of_notMem (mem_Ioi.not.mpr ht), map_zero, ContinuousLinearMap.zero_apply]

Premises used: Iff.mpr, map_zero, Set.mem_Ioi, Iff.not, Set.indicator_of_notMem, ContinuousLinearMap.zero_apply
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
μ ν : Measure ℝ
inst_6 : SFinite μ
inst_7 : SFinite ν
inst_8 : μ.IsAddRightInvariant
inst_9 : NoAtoms ν
hf : IntegrableOn f (Ioi 0) ν
hg : IntegrableOn g (Ioi 0) μ
L : E →L[ℝ] E' →L[ℝ] F
rw :
  ∀ (hf : Integrable (indicator (Ioi 0) f) ν) (hg : Integrable (indicator (Ioi 0) g) μ) (L : E →L[ℝ] E' →L[ℝ] F),
    Integrable (posConvolution f g L ν) μ
⊢ Integrable (posConvolution f g L ν) μ

Tactic:
rw [← integrable_indicator_iff (measurableSet_Ioi : MeasurableSet (Ioi (0 : ℝ)))] at hf hg

Premises used: measurableSet_Ioi, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
μ ν : Measure ℝ
inst_6 : SFinite μ
inst_7 : SFinite ν
inst_8 : μ.IsAddRightInvariant
inst_9 : NoAtoms ν
hf : Integrable (indicator (Ioi 0) f) ν
hg : Integrable (indicator (Ioi 0) g) μ
L : E →L[ℝ] E' →L[ℝ] F
rw : Integrable (indicator (Ioi 0) f ⋆[L, ν] indicator (Ioi 0) g) μ
⊢ Integrable (posConvolution f g L ν) μ

Tactic:
rw [posConvolution_eq_convolution_indicator f g L ν]

Premises used: MeasureTheory.posConvolution_eq_convolution_indicator
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
μ ν : Measure ℝ
inst_6 : SFinite μ
inst_7 : SFinite ν
inst_8 : μ.IsAddRightInvariant
inst_9 : NoAtoms ν
hf : Integrable (indicator (Ioi 0) f) ν
hg : Integrable (indicator (Ioi 0) g) μ
L : E →L[ℝ] E' →L[ℝ] F
⊢ Integrable (indicator (Ioi 0) f ⋆[L, ν] indicator (Ioi 0) g) μ

Tactic:
(hf.convolution_integrand L hg).integral_prod_left

Premises used: MeasureTheory.Integrable.integral_prod_left, MeasureTheory.Integrable.convolution_integrand, MeasureTheory.convolution
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
μ ν : Measure ℝ
inst_6 : SFinite μ
inst_7 : SFinite ν
inst_8 : μ.IsAddRightInvariant
inst_9 : NoAtoms ν
hf : Integrable (indicator (Ioi 0) f) ν
hg : Integrable (indicator (Ioi 0) g) μ
L : E →L[ℝ] E' →L[ℝ] F
⊢ Integrable (indicator (Ioi 0) f ⋆[L, ν] indicator (Ioi 0) g) μ

Tactic:
exact (hf.convolution_integrand L hg).integral_prod_left

Premises used: MeasureTheory.Integrable.integral_prod_left, MeasureTheory.Integrable.convolution_integrand
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
inst_6 : CompleteSpace E
inst_7 : CompleteSpace E'
inst_8 : CompleteSpace F
μ ν : Measure ℝ
inst_9 : SFinite μ
inst_10 : SFinite ν
inst_11 : μ.IsAddRightInvariant
inst_12 : NoAtoms ν
f : ℝ → E
g : ℝ → E'
hf : IntegrableOn f (Ioi 0) ν
hg : IntegrableOn g (Ioi 0) μ
L : E →L[ℝ] E' →L[ℝ] F
rw :
  ∀ (hf : Integrable (indicator (Ioi 0) f) ν) (hg : Integrable (indicator (Ioi 0) g) μ) (L : E →L[ℝ] E' →L[ℝ] F),
    Eq.{uF + 1} (α := F)
      (∫ (x : ℝ) in Ioi 0,
          ∫ (t : ℝ) in 0..x, (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) ∂ν ∂μ :
        F)
      (((L : (a : E) → E' →L[ℝ] F) (∫ (x : ℝ) in Ioi 0, f x ∂ν) : (a : E') → F) (∫ (x : ℝ) in Ioi 0, g x ∂μ) : F)
⊢ Eq.{uF + 1} (α := F)
    (∫ (x : ℝ) in Ioi 0,
        ∫ (t : ℝ) in 0..x, (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) ∂ν ∂μ :
      F)
    (((L : (a : E) → E' →L[ℝ] F) (∫ (x : ℝ) in Ioi 0, f x ∂ν) : (a : E') → F) (∫ (x : ℝ) in Ioi 0, g x ∂μ) : F)

Tactic:
rw [← integrable_indicator_iff measurableSet_Ioi] at hf hg

Premises used: measurableSet_Ioi, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
inst_6 : CompleteSpace E
inst_7 : CompleteSpace E'
inst_8 : CompleteSpace F
μ ν : Measure ℝ
inst_9 : SFinite μ
inst_10 : SFinite ν
inst_11 : μ.IsAddRightInvariant
inst_12 : NoAtoms ν
f : ℝ → E
g : ℝ → E'
hf : Integrable (indicator (Ioi 0) f) ν
hg : Integrable (indicator (Ioi 0) g) μ
L : E →L[ℝ] E' →L[ℝ] F
simp_rw :
  Eq.{uF + 1} (α := F)
    (∫ (x : ℝ),
        indicator (Ioi 0)
          (fun (x : ℝ) ↦
            ∫ (t : ℝ) in 0..x, (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) ∂ν)
          x ∂μ :
      F)
    (((L : (a : E) → E' →L[ℝ] F) (∫ (x : ℝ), indicator (Ioi 0) f x ∂ν) : (a : E') → F)
        (∫ (x : ℝ), indicator (Ioi 0) g x ∂μ) :
      F)
⊢ Eq.{uF + 1} (α := F)
    (∫ (x : ℝ) in Ioi 0,
        ∫ (t : ℝ) in 0..x, (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) ∂ν ∂μ :
      F)
    (((L : (a : E) → E' →L[ℝ] F) (∫ (x : ℝ) in Ioi 0, f x ∂ν) : (a : E') → F) (∫ (x : ℝ) in Ioi 0, g x ∂μ) : F)

Tactic:
simp_rw [← integral_indicator measurableSet_Ioi]

Premises used: MeasureTheory.integral_indicator, measurableSet_Ioi
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
inst_6 : CompleteSpace E
inst_7 : CompleteSpace E'
inst_8 : CompleteSpace F
μ ν : Measure ℝ
inst_9 : SFinite μ
inst_10 : SFinite ν
inst_11 : μ.IsAddRightInvariant
inst_12 : NoAtoms ν
f : ℝ → E
g : ℝ → E'
hf : Integrable (indicator (Ioi 0) f) ν
hg : Integrable (indicator (Ioi 0) g) μ
L : E →L[ℝ] E' →L[ℝ] F
⊢ Eq.{uF + 1} (α := F) (∫ (x : ℝ), (indicator (Ioi 0) f ⋆[L, ν] indicator (Ioi 0) g) x ∂μ : F)
    (((L : (a : E) → E' →L[ℝ] F) (∫ (x : ℝ), indicator (Ioi 0) f x ∂ν) : (a : E') → F)
        (∫ (x : ℝ), indicator (Ioi 0) g x ∂μ) :
      F)

Tactic:
integral_convolution L hf hg

Premises used: MeasureTheory.integral_convolution
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
inst_6 : CompleteSpace E
inst_7 : CompleteSpace E'
inst_8 : CompleteSpace F
μ ν : Measure ℝ
inst_9 : SFinite μ
inst_10 : SFinite ν
inst_11 : μ.IsAddRightInvariant
inst_12 : NoAtoms ν
f : ℝ → E
g : ℝ → E'
hf : Integrable (indicator (Ioi 0) f) ν
hg : Integrable (indicator (Ioi 0) g) μ
L : E →L[ℝ] E' →L[ℝ] F
h :
  ∀ (x : ℝ),
    (indicator (Ioi 0) fun (x : ℝ) ↦
        ∫ (t : ℝ) in 0..x, (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) ∂ν) =
      indicator (Ioi 0) f ⋆[L, ν] indicator (Ioi 0) g
⊢ Eq.{uF + 1} (α := F)
    (∫ (x : ℝ),
        indicator (Ioi 0)
          (fun (x : ℝ) ↦
            ∫ (t : ℝ) in 0..x, (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) ∂ν)
          x ∂μ :
      F)
    (((L : (a : E) → E' →L[ℝ] F) (∫ (x : ℝ), indicator (Ioi 0) f x ∂ν) : (a : E') → F)
        (∫ (x : ℝ), indicator (Ioi 0) g x ∂μ) :
      F)

Tactic:
convert! integral_convolution L hf hg using 4 with x

Premises used: MeasureTheory.integral_convolution
-- Module: Mathlib.Analysis.Convolution
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
inst_6 : CompleteSpace E
inst_7 : CompleteSpace E'
inst_8 : CompleteSpace F
μ ν : Measure ℝ
inst_9 : SFinite μ
inst_10 : SFinite ν
inst_11 : μ.IsAddRightInvariant
inst_12 : NoAtoms ν
f : ℝ → E
g : ℝ → E'
hf : Integrable (indicator (Ioi 0) f) ν
hg : Integrable (indicator (Ioi 0) g) μ
L : E →L[ℝ] E' →L[ℝ] F
x : ℝ
⊢ (indicator (Ioi 0) fun (x : ℝ) ↦
      ∫ (t : ℝ) in 0..x, (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) ∂ν) =
    indicator (Ioi 0) f ⋆[L, ν] indicator (Ioi 0) g

Tactic:
apply posConvolution_eq_convolution_indicator

Premises used: MeasureTheory.posConvolution_eq_convolution_indicator
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
h : ∀ (k : ZMod N), auxDFT (fun (j : ZMod N) ↦ Φ (-j)) k = auxDFT Φ (-k)
⊢ Eq.{u_1 + 1} (α := (k : ZMod N) → E) (auxDFT fun (j : ZMod N) ↦ Φ (-j)) fun (k : ZMod N) ↦ auxDFT Φ (-k)

Tactic:
ext1 k
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
k j : ZMod N
rw :
  HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(j * k)) : ℂ) (Φ (-j)) =
    HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(-j * -k)) : ℂ) (Φ (-j))
rw₁ rw₂ :
  HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(j * k)) : ℂ) (Φ (-j)) =
    HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(j * k)) : ℂ) (Φ (-j))
⊢ HSMul.hSMul (α := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(j * k)) : ℂ) (Φ (-j)) =
    HSMul.hSMul (α := ℂ)
      ((stdAddChar : (a : ZMod N) → ℂ)
          (-HMul.hMul (α := ZMod N) ((Equiv.neg (ZMod N) : (a : ZMod N) → ZMod N) j : ZMod N) (-k)) :
        ℂ)
      (Φ ((Equiv.neg (ZMod N) : (a : ZMod N) → ZMod N) j))

Tactic:
rw [Equiv.neg_apply, neg_mul_neg]

Premises used: Equiv.neg_apply, neg_mul_neg
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
k : ZMod N
⊢ auxDFT (fun (j : ZMod N) ↦ Φ (-j)) k = auxDFT Φ (-k)

Tactic:
simpa only [auxDFT] using
    Fintype.sum_equiv (Equiv.neg _) _ _ (fun j ↦ by rw [Equiv.neg_apply, neg_mul_neg])

Premises used: Equiv.neg, _private.0.ZMod.auxDFT, Fintype.sum_equiv
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
E : Type u_1
inst_1 : AddCommGroup E
inst_2 : Module ℂ E
Φ : ZMod N → E
h : ∀ (j : ZMod N), auxDFT (auxDFT Φ) j = HSMul.hSMul (α := ℂ) (↑N : ℂ) (Φ (-j))
⊢ auxDFT (auxDFT Φ) = fun (j : ZMod N) ↦ HSMul.hSMul (α := ℂ) (↑N : ℂ) (Φ (-j))

Tactic:
ext1 j