awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
D : Type u_4
E : Type u_5
V : Type u_7
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
inst_4 : NormedAddCommGroup V
inst_5 : NormedSpace ℝ V
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : MeasurableSpace D
μ : Measure D
inst_9 : BorelSpace D
inst_10 : FiniteDimensional ℝ D
inst_11 : μ.IsAddHaarMeasure
f : 𝓢(D, E)
g : 𝓢(D, F)
L : E →L[ℝ] F →L[ℝ] V
v : D
hf :
  ∀ (x : D),
    Membership.mem (γ := Set D) (tsupport.{u_4, u_8} (α := F) (⇑g : (a : D) → F)) x →
      HasLineDerivAt.{0, u_5, u_4} ℝ (F := E) ((⇑f : (a : D) → E) : (a : D) → E) ((∂_{v} f : (a : D) → E) x : E) x v
hg :
  ∀ (x : D),
    Membership.mem (γ := Set D) (tsupport.{u_4, u_5} (α := E) (⇑f : (a : D) → E)) x →
      HasLineDerivAt.{0, u_8, u_4} ℝ (F := F) ((⇑g : (a : D) → F) : (a : D) → F) ((∂_{v} g : (a : D) → F) x : F) x v
⊢ Eq.{u_7 + 1} (α := V)
    (∫ (x : D),
      (((L : (a : E) → F →L[ℝ] V) ((f : (a : D) → E) x) : F →L[ℝ] V) : (a : F) → V) ((∂_{v} g : (a : D) → F) x : F) ∂μ)
    (-∫ (x : D),
        (((L : (a : E) → F →L[ℝ] V) ((∂_{v} f : (a : D) → E) x) : F →L[ℝ] V) : (a : F) → V)
          ((g : (a : D) → F) x : F) ∂μ)

Tactic:
apply integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable (v := v)
    (bilinLeftCLM L g.hasTemperateGrowth _).integrable
    (bilinLeftCLM L (∂_{v} g).hasTemperateGrowth _).integrable
    (bilinLeftCLM L g.hasTemperateGrowth _).integrable

Premises used: SchwartzMap.bilinLeftCLM, integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable, SchwartzMap.integrable, DFunLike.coe, SchwartzMap.hasTemperateGrowth
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
D : Type u_4
E : Type u_5
V : Type u_7
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
inst_4 : NormedAddCommGroup V
inst_5 : NormedSpace ℝ V
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : MeasurableSpace D
μ : Measure D
inst_9 : BorelSpace D
inst_10 : FiniteDimensional ℝ D
inst_11 : μ.IsAddHaarMeasure
f : 𝓢(D, E)
g : 𝓢(D, F)
L : E →L[ℝ] F →L[ℝ] V
v : D
⊢ ∀ (x : D),
    Membership.mem (γ := Set D) (tsupport.{u_4, u_8} (α := F) (⇑g : (a : D) → F)) x →
      HasLineDerivAt.{0, u_5, u_4} ℝ (F := E) ((⇑f : (a : D) → E) : (a : D) → E) ((∂_{v} f : (a : D) → E) x : E) x v

Tactic:
fun x _ ↦ (hasFDerivAt _ x).hasLineDerivAt v

Premises used: SchwartzMap.hasFDerivAt, HasFDerivAt.hasLineDerivAt
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
D : Type u_4
E : Type u_5
V : Type u_7
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
inst_4 : NormedAddCommGroup V
inst_5 : NormedSpace ℝ V
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : MeasurableSpace D
μ : Measure D
inst_9 : BorelSpace D
inst_10 : FiniteDimensional ℝ D
inst_11 : μ.IsAddHaarMeasure
f : 𝓢(D, E)
g : 𝓢(D, F)
L : E →L[ℝ] F →L[ℝ] V
v : D
⊢ ∀ (x : D),
    Membership.mem (γ := Set D) (tsupport.{u_4, u_8} (α := F) (⇑g : (a : D) → F)) x →
      HasLineDerivAt.{0, u_5, u_4} ℝ (F := E) ((⇑f : (a : D) → E) : (a : D) → E) ((∂_{v} f : (a : D) → E) x : E) x v

Tactic:
exact fun x _ ↦ (hasFDerivAt _ x).hasLineDerivAt v

Premises used: SchwartzMap.hasFDerivAt, HasFDerivAt.hasLineDerivAt
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
D : Type u_4
E : Type u_5
V : Type u_7
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
inst_4 : NormedAddCommGroup V
inst_5 : NormedSpace ℝ V
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : MeasurableSpace D
μ : Measure D
inst_9 : BorelSpace D
inst_10 : FiniteDimensional ℝ D
inst_11 : μ.IsAddHaarMeasure
f : 𝓢(D, E)
g : 𝓢(D, F)
L : E →L[ℝ] F →L[ℝ] V
v : D
⊢ ∀ (x : D),
    Membership.mem (γ := Set D) (tsupport.{u_4, u_5} (α := E) (⇑f : (a : D) → E)) x →
      HasLineDerivAt.{0, u_8, u_4} ℝ (F := F) ((⇑g : (a : D) → F) : (a : D) → F) ((∂_{v} g : (a : D) → F) x : F) x v

Tactic:
fun x _ ↦ (hasFDerivAt _ x).hasLineDerivAt v

Premises used: SchwartzMap.hasFDerivAt, HasFDerivAt.hasLineDerivAt
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
D : Type u_4
E : Type u_5
V : Type u_7
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
inst_4 : NormedAddCommGroup V
inst_5 : NormedSpace ℝ V
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : MeasurableSpace D
μ : Measure D
inst_9 : BorelSpace D
inst_10 : FiniteDimensional ℝ D
inst_11 : μ.IsAddHaarMeasure
f : 𝓢(D, E)
g : 𝓢(D, F)
L : E →L[ℝ] F →L[ℝ] V
v : D
⊢ ∀ (x : D),
    Membership.mem (γ := Set D) (tsupport.{u_4, u_5} (α := E) (⇑f : (a : D) → E)) x →
      HasLineDerivAt.{0, u_8, u_4} ℝ (F := F) ((⇑g : (a : D) → F) : (a : D) → F) ((∂_{v} g : (a : D) → F) x : F) x v

Tactic:
exact fun x _ ↦ (hasFDerivAt _ x).hasLineDerivAt v

Premises used: SchwartzMap.hasFDerivAt, HasFDerivAt.hasLineDerivAt
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
𝕜 : Type u_2
D : Type u_4
inst : NormedAddCommGroup D
inst_1 : NormedSpace ℝ D
inst_2 : MeasurableSpace D
μ : Measure D
inst_3 : BorelSpace D
inst_4 : FiniteDimensional ℝ D
inst_5 : μ.IsAddHaarMeasure
inst_6 : NormedRing 𝕜
inst_7 : NormedSpace ℝ 𝕜
inst_8 : IsScalarTower ℝ 𝕜 𝕜
inst_9 : SMulCommClass ℝ 𝕜 𝕜
f g : 𝓢(D, 𝕜)
v : D
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (∫ (x : D), HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : D) → 𝕜) x : 𝕜) ((∂_{v} g : (a : D) → 𝕜) x : 𝕜) ∂μ)
    (-∫ (x : D), HMul.hMul (α := 𝕜) (β := 𝕜) ((∂_{v} f : (a : D) → 𝕜) x : 𝕜) ((g : (a : D) → 𝕜) x : 𝕜) ∂μ)

Tactic:
integral_bilinear_lineDerivOp_right_eq_neg_left f g (ContinuousLinearMap.mul ℝ 𝕜) v

Premises used: Real, ContinuousLinearMap.mul, SchwartzMap.integral_bilinear_lineDerivOp_right_eq_neg_left
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
𝕜 : Type u_2
D : Type u_4
F : Type u_8
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup D
inst_3 : NormedSpace ℝ D
inst_4 : MeasurableSpace D
μ : Measure D
inst_5 : BorelSpace D
inst_6 : FiniteDimensional ℝ D
inst_7 : μ.IsAddHaarMeasure
inst_8 : RCLike 𝕜
inst_9 : NormedSpace 𝕜 F
f : 𝓢(D, 𝕜)
g : 𝓢(D, F)
v : D
⊢ Eq.{u_8 + 1} (α := F)
    (∫ (x : D),
      HSMul.hSMul.{u_2, u_8, u_8} (α := 𝕜) (β := F) ((f : (a : D) → 𝕜) x : 𝕜) ((∂_{v} g : (a : D) → F) x : F) ∂μ)
    (-∫ (x : D),
        HSMul.hSMul.{u_2, u_8, u_8} (α := 𝕜) (β := F) ((∂_{v} f : (a : D) → 𝕜) x : 𝕜) ((g : (a : D) → F) x : F) ∂μ)

Tactic:
integral_bilinear_lineDerivOp_right_eq_neg_left f g (ContinuousLinearMap.lsmul ℝ 𝕜) v

Premises used: Real, SchwartzMap.integral_bilinear_lineDerivOp_right_eq_neg_left, ContinuousLinearMap.lsmul
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
𝕜 : Type u_2
D : Type u_4
V : Type u_7
F : Type u_8
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
inst_6 : MeasurableSpace D
μ : Measure D
inst_7 : BorelSpace D
inst_8 : FiniteDimensional ℝ D
inst_9 : μ.IsAddHaarMeasure
inst_10 : RCLike 𝕜
inst_11 : NormedSpace 𝕜 F
inst_12 : NormedSpace 𝕜 V
f : 𝓢(D, F →L[𝕜] V)
g : 𝓢(D, F)
v : D
⊢ Eq.{u_7 + 1} (α := V)
    (∫ (x : D), (((f : (a : D) → F →L[𝕜] V) x : F →L[𝕜] V) : (a : F) → V) ((∂_{v} g : (a : D) → F) x : F) ∂μ)
    (-∫ (x : D), (((∂_{v} f : (a : D) → F →L[𝕜] V) x : F →L[𝕜] V) : (a : F) → V) ((g : (a : D) → F) x : F) ∂μ)

Tactic:
integral_bilinear_lineDerivOp_right_eq_neg_left f g
    ((ContinuousLinearMap.id 𝕜 (F →L[𝕜] V)).bilinearRestrictScalars ℝ) v

Premises used: Real, ContinuousLinearMap.id, ContinuousLinearMap, SchwartzMap.integral_bilinear_lineDerivOp_right_eq_neg_left, ContinuousLinearMap.bilinearRestrictScalars, RingHom.id
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace ℝ F₁
inst_5 : NormedAddCommGroup F₂
inst_6 : NormedSpace ℝ F₂
inst_7 : NormedAddCommGroup F₃
inst_8 : NormedSpace ℝ F₃
inst_9 : MeasurableSpace E
μ : Measure E
inst_10 : BorelSpace E
inst_11 : μ.IsAddHaarMeasure
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
L : F₁ →L[ℝ] F₂ →L[ℝ] F₃
simp_rw :
  Eq.{u_11 + 1} (α := F₃)
    (∫ (x : E),
      ∑ x_1 : Fin (Module.finrank ℝ E),
        (((L : (a : F₁) → F₂ →L[ℝ] F₃) ((f : (a : E) → F₁) x) : F₂ →L[ℝ] F₃) : (a : F₂) → F₃)
          ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) x_1 : E)
                  (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) x_1 : E) g) :
                (a : E) → F₂)
              x :
            F₂) ∂μ)
    (∫ (x : E),
      ∑ c : Fin (Module.finrank ℝ E),
        (((L : (a : F₁) → F₂ →L[ℝ] F₃)
                ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) c : E)
                      (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) c : E) f) :
                    (a : E) → F₁)
                  x) :
              F₂ →L[ℝ] F₃) :
            (a : F₂) → F₃)
          ((g : (a : E) → F₂) x : F₂) ∂μ)
⊢ Eq.{u_11 + 1} (α := F₃)
    (∫ (x : E),
      (((L : (a : F₁) → F₂ →L[ℝ] F₃) ((f : (a : E) → F₁) x) : F₂ →L[ℝ] F₃) : (a : F₂) → F₃)
        ((Δ g : (a : E) → F₂) x : F₂) ∂μ)
    (∫ (x : E),
      (((L : (a : F₁) → F₂ →L[ℝ] F₃) ((Δ f : (a : E) → F₁) x) : F₂ →L[ℝ] F₃) : (a : F₂) → F₃)
        ((g : (a : E) → F₂) x : F₂) ∂μ)

Tactic:
simp_rw [laplacian_eq_sum (stdOrthonormalBasis ℝ E), sum_apply, map_sum,
    ContinuousLinearMap.coe_sum', Finset.sum_apply]

Premises used: Real, Finset.sum_apply, map_sum, ContinuousLinearMap.coe_sum', SchwartzMap.sum_apply, SchwartzMap.laplacian_eq_sum, stdOrthonormalBasis
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace ℝ F₁
inst_5 : NormedAddCommGroup F₂
inst_6 : NormedSpace ℝ F₂
inst_7 : NormedAddCommGroup F₃
inst_8 : NormedSpace ℝ F₃
inst_9 : MeasurableSpace E
μ : Measure E
inst_10 : BorelSpace E
inst_11 : μ.IsAddHaarMeasure
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
L : F₁ →L[ℝ] F₂ →L[ℝ] F₃
⊢ Eq.{u_11 + 1} (α := F₃)
    (∑ i : Fin (Module.finrank ℝ E),
      ∫ (a : E),
        (((L : (a : F₁) → F₂ →L[ℝ] F₃) ((f : (a : E) → F₁) a) : F₂ →L[ℝ] F₃) : (a : F₂) → F₃)
          ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E)
                  (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E) g) :
                (a : E) → F₂)
              a :
            F₂) ∂μ)
    (∑ i : Fin (Module.finrank ℝ E),
      ∫ (a : E),
        (((L : (a : F₁) → F₂ →L[ℝ] F₃)
                ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E)
                      (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E) f) :
                    (a : E) → F₁)
                  a) :
              F₂ →L[ℝ] F₃) :
            (a : F₂) → F₃)
          ((g : (a : E) → F₂) a : F₂) ∂μ)

Tactic:
simp [integral_bilinear_lineDerivOp_right_eq_neg_left]

Premises used: SchwartzMap.integral_bilinear_lineDerivOp_right_eq_neg_left
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace ℝ F₁
inst_5 : NormedAddCommGroup F₂
inst_6 : NormedSpace ℝ F₂
inst_7 : NormedAddCommGroup F₃
inst_8 : NormedSpace ℝ F₃
inst_9 : MeasurableSpace E
μ : Measure E
inst_10 : BorelSpace E
inst_11 : μ.IsAddHaarMeasure
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
L : F₁ →L[ℝ] F₂ →L[ℝ] F₃
⊢ ∀ (i : Fin (Module.finrank ℝ E)),
    Membership.mem (γ := Finset (Fin (Module.finrank ℝ E))) Finset.univ i →
      Integrable.{u_11, u_5} (ε := F₃)
        (fun (x : E) ↦
          (((L : (a : F₁) → F₂ →L[ℝ] F₃)
                  ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E)
                        (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E)
                          f) :
                      (a : E) → F₁)
                    x) :
                F₂ →L[ℝ] F₃) :
              (a : F₂) → F₃)
            ((g : (a : E) → F₂) x : F₂))
        μ

Tactic:
fun _ _ ↦ (pairing L (∂_{_} <| ∂_{_} f) g).integrable

Premises used: Real, SchwartzMap.pairing, LineDeriv.lineDerivOp, SchwartzMap.integrable, DFunLike.coe, stdOrthonormalBasis
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace ℝ F₁
inst_5 : NormedAddCommGroup F₂
inst_6 : NormedSpace ℝ F₂
inst_7 : NormedAddCommGroup F₃
inst_8 : NormedSpace ℝ F₃
inst_9 : MeasurableSpace E
μ : Measure E
inst_10 : BorelSpace E
inst_11 : μ.IsAddHaarMeasure
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
L : F₁ →L[ℝ] F₂ →L[ℝ] F₃
⊢ ∀ (i : Fin (Module.finrank ℝ E)),
    Membership.mem (γ := Finset (Fin (Module.finrank ℝ E))) Finset.univ i →
      Integrable.{u_11, u_5} (ε := F₃)
        (fun (x : E) ↦
          (((L : (a : F₁) → F₂ →L[ℝ] F₃)
                  ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E)
                        (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E)
                          f) :
                      (a : E) → F₁)
                    x) :
                F₂ →L[ℝ] F₃) :
              (a : F₂) → F₃)
            ((g : (a : E) → F₂) x : F₂))
        μ

Tactic:
exact fun _ _ ↦ (pairing L (∂_{_} <| ∂_{_} f) g).integrable

Premises used: SchwartzMap.pairing, LineDeriv.lineDerivOp, SchwartzMap.integrable, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace ℝ F₁
inst_5 : NormedAddCommGroup F₂
inst_6 : NormedSpace ℝ F₂
inst_7 : NormedAddCommGroup F₃
inst_8 : NormedSpace ℝ F₃
inst_9 : MeasurableSpace E
μ : Measure E
inst_10 : BorelSpace E
inst_11 : μ.IsAddHaarMeasure
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
L : F₁ →L[ℝ] F₂ →L[ℝ] F₃
⊢ ∀ (i : Fin (Module.finrank ℝ E)),
    Membership.mem (γ := Finset (Fin (Module.finrank ℝ E))) Finset.univ i →
      Integrable.{u_11, u_5} (ε := F₃)
        (fun (x : E) ↦
          (((L : (a : F₁) → F₂ →L[ℝ] F₃) ((f : (a : E) → F₁) x) : F₂ →L[ℝ] F₃) : (a : F₂) → F₃)
            ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E)
                    (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E) g) :
                  (a : E) → F₂)
                x :
              F₂))
        μ

Tactic:
fun _ _ ↦ (pairing L f (∂_{_} <| ∂_{_} g)).integrable

Premises used: Real, SchwartzMap.pairing, LineDeriv.lineDerivOp, SchwartzMap.integrable, DFunLike.coe, stdOrthonormalBasis
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace ℝ F₁
inst_5 : NormedAddCommGroup F₂
inst_6 : NormedSpace ℝ F₂
inst_7 : NormedAddCommGroup F₃
inst_8 : NormedSpace ℝ F₃
inst_9 : MeasurableSpace E
μ : Measure E
inst_10 : BorelSpace E
inst_11 : μ.IsAddHaarMeasure
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
L : F₁ →L[ℝ] F₂ →L[ℝ] F₃
⊢ ∀ (i : Fin (Module.finrank ℝ E)),
    Membership.mem (γ := Finset (Fin (Module.finrank ℝ E))) Finset.univ i →
      Integrable.{u_11, u_5} (ε := F₃)
        (fun (x : E) ↦
          (((L : (a : F₁) → F₂ →L[ℝ] F₃) ((f : (a : E) → F₁) x) : F₂ →L[ℝ] F₃) : (a : F₂) → F₃)
            ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E)
                    (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E) g) :
                  (a : E) → F₂)
                x :
              F₂))
        μ

Tactic:
exact fun _ _ ↦ (pairing L f (∂_{_} <| ∂_{_} g)).integrable

Premises used: SchwartzMap.pairing, LineDeriv.lineDerivOp, SchwartzMap.integrable, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
𝕜 : Type u_2
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : μ.IsAddHaarMeasure
inst_6 : NormedRing 𝕜
inst_7 : NormedSpace ℝ 𝕜
inst_8 : IsScalarTower ℝ 𝕜 𝕜
inst_9 : SMulCommClass ℝ 𝕜 𝕜
f g : 𝓢(E, 𝕜)
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (∫ (x : E), HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : E) → 𝕜) x : 𝕜) ((Δ g : (a : E) → 𝕜) x : 𝕜) ∂μ)
    (∫ (x : E), HMul.hMul (α := 𝕜) (β := 𝕜) ((Δ f : (a : E) → 𝕜) x : 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ∂μ)

Tactic:
integral_bilinear_laplacian_right_eq_left f g (ContinuousLinearMap.mul ℝ 𝕜)

Premises used: Real, SchwartzMap.integral_bilinear_laplacian_right_eq_left, ContinuousLinearMap.mul
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : InnerProductSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : MeasurableSpace E
μ : Measure E
inst_6 : BorelSpace E
inst_7 : μ.IsAddHaarMeasure
inst_8 : RCLike 𝕜
inst_9 : NormedSpace 𝕜 F
f : 𝓢(E, 𝕜)
g : 𝓢(E, F)
⊢ Eq.{u_8 + 1} (α := F)
    (∫ (x : E), HSMul.hSMul.{u_2, u_8, u_8} (α := 𝕜) (β := F) ((f : (a : E) → 𝕜) x : 𝕜) ((Δ g : (a : E) → F) x : F) ∂μ)
    (∫ (x : E), HSMul.hSMul.{u_2, u_8, u_8} (α := 𝕜) (β := F) ((Δ f : (a : E) → 𝕜) x : 𝕜) ((g : (a : E) → F) x : F) ∂μ)

Tactic:
integral_bilinear_laplacian_right_eq_left f g (ContinuousLinearMap.lsmul ℝ 𝕜)

Premises used: Real, SchwartzMap.integral_bilinear_laplacian_right_eq_left, ContinuousLinearMap.lsmul
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
𝕜 : Type u_2
E : Type u_5
F₁ : Type u_9
F₂ : Type u_10
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace ℝ F₁
inst_5 : NormedAddCommGroup F₂
inst_6 : NormedSpace ℝ F₂
inst_7 : MeasurableSpace E
μ : Measure E
inst_8 : BorelSpace E
inst_9 : μ.IsAddHaarMeasure
inst_10 : RCLike 𝕜
inst_11 : NormedSpace 𝕜 F₁
inst_12 : NormedSpace 𝕜 F₂
f : 𝓢(E, F₁ →L[𝕜] F₂)
g : 𝓢(E, F₁)
⊢ Eq.{u_10 + 1} (α := F₂)
    (∫ (x : E), (((f : (a : E) → F₁ →L[𝕜] F₂) x : F₁ →L[𝕜] F₂) : (a : F₁) → F₂) ((Δ g : (a : E) → F₁) x : F₁) ∂μ)
    (∫ (x : E), (((Δ f : (a : E) → F₁ →L[𝕜] F₂) x : F₁ →L[𝕜] F₂) : (a : F₁) → F₂) ((g : (a : E) → F₁) x : F₁) ∂μ)

Tactic:
integral_bilinear_laplacian_right_eq_left f g
    ((ContinuousLinearMap.id 𝕜 (F₁ →L[𝕜] F₂)).bilinearRestrictScalars ℝ)

Premises used: Real, ContinuousLinearMap.id, ContinuousLinearMap, SchwartzMap.integral_bilinear_laplacian_right_eq_left, ContinuousLinearMap.bilinearRestrictScalars, RingHom.id
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
refine_1 :
  ∀ (f g : 𝓢(V, E)) (x : V),
    (fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) (f + g) x =
      HAdd.hAdd (α := E) ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f x)
        ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) g x)
refine_2 :
  ∀ (a : 𝕜) (f : 𝓢(V, E)) (x : V),
    (fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) (a • f) x =
      HSMul.hSMul (α := 𝕜) (β := E) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜)
        ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f x)
refine_3 :
  ∀ (f : 𝓢(V, E)),
    ContDiff.{0, u_3, u_2} ℝ (E := V) (F := E) (↑⊤ : WithTop ℕ∞)
      ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f)
refine_4 :
  ∀ (n : ℕ × ℕ),
    ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
      0 ≤ C ∧
        ∀ (f : 𝓢(V, E)) (x : V),
          ‖x‖ ^ n.1 *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin n.2) ↦ V) E)
                (iteratedFDeriv ℝ n.2 ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f) x) ≤
            HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 V E) : (a : 𝓢(V, E)) → ℝ) f : ℝ)
⊢ 𝓢(V, E) →L[𝕜] 𝓢(V, E)

Tactic:
refine mkCLM ((𝓕 : (V → E) → (V → E)) ·) ?_ ?_ ?_ ?_

Premises used: SchwartzMap.mkCLM, FourierTransform.fourier, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
f g : 𝓢(V, E)
⊢ ∀ (x : V),
    (fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) (f + g) x =
      HAdd.hAdd (α := E) ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f x)
        ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) g x)

Tactic:
simp [fourier_eq, integral_add ((fourierIntegral_convergent_iff _).mpr f.integrable)
      ((fourierIntegral_convergent_iff _).mpr g.integrable)]

Premises used: Iff.mpr, Real.fourier_eq, Real.fourierIntegral_convergent_iff, SchwartzMap.integrable, MeasureTheory.integral_add
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
⊢ ∀ (a : 𝕜) (f : 𝓢(V, E)) (x : V),
    (fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) (a • f) x =
      HSMul.hSMul (α := 𝕜) (β := E) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜)
        ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f x)

Tactic:
simp [fourier_eq, smul_comm, integral_smul]

Premises used: MeasureTheory.integral_smul, Real.fourier_eq, SMulCommClass.smul_comm
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
⊢ ∀ (f : 𝓢(V, E)),
    ContDiff.{0, u_3, u_2} ℝ (E := V) (F := E) (↑⊤ : WithTop ℕ∞)
      ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f)

Tactic:
fun f ↦ contDiff_fourier (fun n _ ↦ integrable_pow_mul volume f n)

Premises used: Real.contDiff_fourier, MeasureTheory.MeasureSpace.volume, SchwartzMap.integrable_pow_mul
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
⊢ ∀ (f : 𝓢(V, E)),
    ContDiff.{0, u_3, u_2} ℝ (E := V) (F := E) (↑⊤ : WithTop ℕ∞)
      ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f)

Tactic:
exact fun f ↦ contDiff_fourier (fun n _ ↦ integrable_pow_mul volume f n)

Premises used: Real.contDiff_fourier