awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
m : MeasurableSpace E
inst_11 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_12 : NormedAddCommGroup F₁
inst_13 : NormedSpace 𝕜 F₁
inst_14 : NormedSpace ℝ F₁
inst_15 : NormedAddCommGroup F₂
inst_16 : NormedSpace 𝕜 F₂
inst_17 : NormedAddCommGroup F₃
inst_18 : NormedSpace 𝕜 F₃
inst_19 : SMulCommClass ℝ 𝕜 F₁
inst_20 : NormedSpace ℝ F₃
inst_21 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f g : 𝓓^{n}_{K}(E, F₁)
hφ : ¬IntegrableOn φ (↑K : Set E) μ
⊢ 0 = HAdd.hAdd (α := F₃) 0 0

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
m : MeasurableSpace E
inst_11 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_12 : NormedAddCommGroup F₁
inst_13 : NormedSpace 𝕜 F₁
inst_14 : NormedSpace ℝ F₁
inst_15 : NormedAddCommGroup F₂
inst_16 : NormedSpace 𝕜 F₂
inst_17 : NormedAddCommGroup F₃
inst_18 : NormedSpace 𝕜 F₃
inst_19 : SMulCommClass ℝ 𝕜 F₁
inst_20 : NormedSpace ℝ F₃
inst_21 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
c : 𝕜
f : 𝓓^{n}_{K}(E, F₁)
pos :
  ∀ (hφ : IntegrableOn φ (↑K : Set E) μ),
    ∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((c • f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ =
      HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
        (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
neg : ∀ (hφ : ¬IntegrableOn φ (↑K : Set E) μ), 0 = HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) 0
⊢ (if IntegrableOn φ (↑K : Set E) μ then
      ∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((c • f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ
    else 0) =
    HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (if IntegrableOn φ (↑K : Set E) μ then
        ∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ
      else 0)

Tactic:
split_ifs with hφ
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
m : MeasurableSpace E
inst_11 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_12 : NormedAddCommGroup F₁
inst_13 : NormedSpace 𝕜 F₁
inst_14 : NormedSpace ℝ F₁
inst_15 : NormedAddCommGroup F₂
inst_16 : NormedSpace 𝕜 F₂
inst_17 : NormedAddCommGroup F₃
inst_18 : NormedSpace 𝕜 F₃
inst_19 : SMulCommClass ℝ 𝕜 F₁
inst_20 : NormedSpace ℝ F₃
inst_21 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
c : 𝕜
f : 𝓓^{n}_{K}(E, F₁)
hφ : ¬IntegrableOn φ (↑K : Set E) μ
⊢ 0 = HSMul.hSMul (α := 𝕜) (β := F₃) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
⊢ Eq.{u_7 + 1} (α := F₃) ((integralAgainstBilinLM B μ φ : (a : 𝓓^{n}_{K}(E, F₁)) → F₃) f : F₃)
    (if IntegrableOn φ (↑K : Set E) μ then
        ∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ
      else 0 :
      F₃)

Tactic:
rfl
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K : Set E) μ
f : 𝓓^{n}_{K}(E, F₁)
⊢ Eq.{u_7 + 1} (α := F₃) ((integralAgainstBilinLM B μ φ : (a : 𝓓^{n}_{K}(E, F₁)) → F₃) f : F₃)
    (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ : F₃)

Tactic:
simp [hφ]
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K : Set E) μ
f : 𝓓^{n}_{K}(E, F₁)
rw :
  ∀ x ∉ (↑K : Set E),
    Eq.{u_7 + 1} (α := F₃)
      ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃) (0 : F₃)
⊢ Eq.{u_7 + 1} (α := F₃) ((integralAgainstBilinLM B μ φ : (a : 𝓓^{n}_{K}(E, F₁)) → F₃) f : F₃)
    (∫ (x : E) in (↑K : Set E),
        (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ :
      F₃)

Tactic:
rw [integralAgainstBilinLM_eq_integral hφ, setIntegral_eq_integral_of_forall_compl_eq_zero]

Premises used: MeasureTheory.setIntegral_eq_integral_of_forall_compl_eq_zero, ContDiffMapSupportedIn.integralAgainstBilinLM_eq_integral
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K : Set E) μ
f : 𝓓^{n}_{K}(E, F₁)
x : E
hx : x ∉ (↑K : Set E)
rw : Eq.{u_7 + 1} (α := F₃) (((B : (a : F₁) → F₂ →L[𝕜] F₃) (0 x) : (a : F₂) → F₃) (φ x) : F₃) (0 : F₃)
rw₁ : Eq.{u_7 + 1} (α := F₃) (((B : (a : F₁) → F₂ →L[𝕜] F₃) 0 : (a : F₂) → F₃) (φ x) : F₃) (0 : F₃)
rw₂ : Eq.{u_7 + 1} (α := F₃) ((0 : (a : F₂) → F₃) (φ x) : F₃) (0 : F₃)
rw₃ rw₄ : Eq.{u_7 + 1} (α := F₃) 0 0
⊢ Eq.{u_7 + 1} (α := F₃)
    ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃) (0 : F₃)

Tactic:
rw [f.zero_on_compl hx, Pi.zero_apply, map_zero, ContinuousLinearMap.zero_apply]

Premises used: Pi.zero_apply, map_zero, ContDiffMapSupportedIn.zero_on_compl, ContinuousLinearMap.zero_apply
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
pos :
  ∀ (hφ : IntegrableOn φ (↑K : Set E) μ),
    norm.{u_7} (E := F₃) ((integralAgainstBilinLM B μ φ : (a : 𝓓^{n}_{K}(E, F₁)) → F₃) f : F₃) ≤
      HMul.hMul (β := ℝ) ((∫ (x : E) in (↑K : Set E), ‖φ x‖ ∂μ) * ‖B‖)
        ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
neg :
  ∀ (hφ : ¬IntegrableOn φ (↑K : Set E) μ),
    norm.{u_7} (E := F₃) ((integralAgainstBilinLM B μ φ : (a : 𝓓^{n}_{K}(E, F₁)) → F₃) f : F₃) ≤
      HMul.hMul (β := ℝ) ((∫ (x : E) in (↑K : Set E), ‖φ x‖ ∂μ) * ‖B‖)
        ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
⊢ norm.{u_7} (E := F₃) ((integralAgainstBilinLM B μ φ : (a : 𝓓^{n}_{K}(E, F₁)) → F₃) f : F₃) ≤
    HMul.hMul (β := ℝ) ((∫ (x : E) in (↑K : Set E), ‖φ x‖ ∂μ) * ‖B‖)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)

Tactic:
by_cases hφ : IntegrableOn φ K μ

Premises used: MeasureTheory.IntegrableOn, SetLike.coe
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K : Set E) μ
h :
  ∀ (x : E),
    norm.{u_7} (E := F₃)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃) ≤
      HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖)
        ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
⊢ ∀ᵐ (x : E) ∂μ.restrict (↑K : Set E),
    norm.{u_7} (E := F₃)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃) ≤
      HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖)
        ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)

Tactic:
filter_upwards [] with x
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K : Set E) μ
x : E
h :
  norm (E := F₂ →L[𝕜] F₃) ((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) * ‖φ x‖ ≤
    HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖) ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
h₁ :
  ‖B‖ * ‖(f : (a : E) → F₁) x‖ * ‖φ x‖ ≤
    HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖) ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
h₂ :
  HMul.hMul (β := ℝ) ‖B‖ ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ) * ‖φ x‖ ≤
    HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖) ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
h₃ :
  ‖φ x‖ * HMul.hMul (β := ℝ) ‖B‖ ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ) ≤
    HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖) ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
h₄ h₅ :
  ‖φ x‖ * HMul.hMul (β := ℝ) ‖B‖ ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ) ≤
    ‖φ x‖ * HMul.hMul (β := ℝ) ‖B‖ ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
⊢ norm.{u_7} (E := F₃)
      ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃) ≤
    HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖) ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)

Tactic:
grw [ContinuousLinearMap.le_opNorm, ContinuousLinearMap.le_opNorm, norm_apply_le_seminorm 𝕜,
        mul_comm, mul_assoc]

Premises used: ContinuousLinearMap.le_opNorm, mul_assoc, ContDiffMapSupportedIn.norm_apply_le_seminorm, mul_comm
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K : Set E) μ
⊢ ∀ᵐ (x : E) ∂μ.restrict (↑K : Set E),
    norm.{u_7} (E := F₃)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃) ≤
      HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖)
        ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)

Tactic:
have h : ∀ᵐ x ∂(μ.restrict K), ‖B (f x) (φ x)‖ ≤ ‖φ x‖ * ‖B‖ * N[𝕜]_{K, n, 0} f := by
      filter_upwards [] with x
      grw [ContinuousLinearMap.le_opNorm, ContinuousLinearMap.le_opNorm, norm_apply_le_seminorm 𝕜,
        mul_comm, mul_assoc]
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K : Set E) μ
h :
  ∀ᵐ (x : E) ∂μ.restrict (↑K : Set E),
    norm.{u_7} (E := F₃)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃) ≤
      HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖)
        ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
pos :
  norm.{u_7} (E := F₃)
      (∫ (x : E) in (↑K : Set E),
        (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ) ≤
    HMul.hMul (β := ℝ) ((∫ (x : E) in (↑K : Set E), ‖φ x‖ ∂μ) * ‖B‖)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
⊢ norm.{u_7} (E := F₃) ((integralAgainstBilinLM B μ φ : (a : 𝓓^{n}_{K}(E, F₁)) → F₃) f : F₃) ≤
    HMul.hMul (β := ℝ) ((∫ (x : E) in (↑K : Set E), ‖φ x‖ ∂μ) * ‖B‖)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)

Tactic:
rw [integralAgainstBilinLM_eq_setIntegral hφ]

Premises used: ContDiffMapSupportedIn.integralAgainstBilinLM_eq_setIntegral
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K : Set E) μ
h :
  ∀ᵐ (x : E) ∂μ.restrict (↑K : Set E),
    norm.{u_7} (E := F₃)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃) ≤
      HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖)
        ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
pos :
  ∫ (x : E) in (↑K : Set E),
      HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖)
        ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ) ∂μ ≤
    HMul.hMul (β := ℝ) ((∫ (x : E) in (↑K : Set E), ‖φ x‖ ∂μ) * ‖B‖)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
⊢ norm.{u_7} (E := F₃)
      (∫ (x : E) in (↑K : Set E),
        (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ) ≤
    HMul.hMul (β := ℝ) ((∫ (x : E) in (↑K : Set E), ‖φ x‖ ∂μ) * ‖B‖)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)

Tactic:
apply le_trans (norm_integral_le_of_norm_le ((hφ.norm.mul_const _).mul_const _) h)

Premises used: MeasureTheory.norm_integral_le_of_norm_le, MeasureTheory.Integrable.mul_const, MeasureTheory.Integrable.norm, le_trans
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K : Set E) μ
h :
  ∀ᵐ (x : E) ∂μ.restrict (↑K : Set E),
    norm.{u_7} (E := F₃)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃) ≤
      HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖)
        ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
pos :
  HMul.hMul (α := ℝ) (β := ℝ) (∫ (a : E) in (↑K : Set E), ‖φ a‖ * ‖B‖ ∂μ : ℝ)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ) ≤
    HMul.hMul (β := ℝ) ((∫ (x : E) in (↑K : Set E), ‖φ x‖ ∂μ) * ‖B‖)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
pos₁ pos₂ :
  HMul.hMul (β := ℝ) ((∫ (a : E) in (↑K : Set E), ‖φ a‖ ∂μ) * ‖B‖)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ) ≤
    HMul.hMul (β := ℝ) ((∫ (a : E) in (↑K : Set E), ‖φ a‖ ∂μ) * ‖B‖)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
⊢ ∫ (x : E) in (↑K : Set E),
      HMul.hMul (β := ℝ) (‖φ x‖ * ‖B‖)
        ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ) ∂μ ≤
    HMul.hMul (β := ℝ) ((∫ (x : E) in (↑K : Set E), ‖φ x‖ ∂μ) * ‖B‖)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)

Tactic:
rw [integral_mul_const, integral_mul_const]

Premises used: MeasureTheory.integral_mul_const
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
hφ : ¬IntegrableOn φ (↑K : Set E) μ
neg :
  0 ≤
    HMul.hMul (β := ℝ) ((∫ (x : E) in (↑K : Set E), ‖φ x‖ ∂μ) * ‖B‖)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)
⊢ norm.{u_7} (E := F₃) ((integralAgainstBilinLM B μ φ : (a : 𝓓^{n}_{K}(E, F₁)) → F₃) f : F₃) ≤
    HMul.hMul (β := ℝ) ((∫ (x : E) in (↑K : Set E), ‖φ x‖ ∂μ) * ‖B‖)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)

Tactic:
simp only [integralAgainstBilinLM, hφ, ↓reduceIte, LinearMap.coe_mk, AddHom.coe_mk, norm_zero]

Premises used: LinearMap.coe_mk, norm_zero, ContDiffMapSupportedIn.integralAgainstBilinLM, reduceIte, AddHom.coe_mk
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
inst_11 : SMulCommClass ℝ 𝕜 F₁
inst_12 : NormedSpace ℝ F₃
inst_13 : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
hφ : ¬IntegrableOn φ (↑K : Set E) μ
⊢ 0 ≤
    HMul.hMul (β := ℝ) ((∫ (x : E) in (↑K : Set E), ‖φ x‖ ∂μ) * ‖B‖)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0 : (a : 𝓓^{n}_{K}(E, F₁)) → ℝ) f : ℝ)

Tactic:
positivity