awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
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
n k : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
hk : n < k + 1
⊢ LE.le (α := ℝ)
    (((ContDiffMapSupportedIn.seminorm 𝕜 E (E →L[ℝ] F) k K i : Seminorm 𝕜 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
          (a : 𝓓^{k}_{K}(E, E →L[ℝ] F)) → ℝ)
        ((fderivLM 𝕜 n k : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F)) f : 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
      ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n K (i + 1) : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)

Tactic:
simp [fderivLM_apply_of_gt 𝕜 f hk]

Premises used: ContDiffMapSupportedIn.fderivLM_apply_of_gt
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
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
K : Compacts E
i : ℕ
f : 𝓓_{K}(E, F)
⊢ Eq (α := ℝ)
    (((ContDiffMapSupportedIn.seminorm 𝕜 E (E →L[ℝ] F) ⊤ K i : Seminorm 𝕜 𝓓_{K}(E, E →L[ℝ] F)) :
          (a : 𝓓_{K}(E, E →L[ℝ] F)) → ℝ)
        ((fderivLM 𝕜 ⊤ ⊤ : (a : 𝓓_{K}(E, F)) → 𝓓_{K}(E, E →L[ℝ] F)) f : 𝓓_{K}(E, E →L[ℝ] F)) :
      ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F ⊤ K (i + 1) : (a : 𝓓_{K}(E, F)) → ℝ) f : ℝ)

Tactic:
simp [ContDiffMapSupportedIn.seminorm_apply, BoundedContinuousFunction.norm_eq_iSup_norm,
    norm_iteratedFDeriv_fderiv]

Premises used: ContDiffMapSupportedIn.seminorm_apply, BoundedContinuousFunction.norm_eq_iSup_norm, norm_iteratedFDeriv_fderiv
-- 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
⊢ Continuous (X := 𝓓^{n}_{K}(E, F)) (Y := 𝓓^{k}_{K}(E, E →L[ℝ] F))
    (⇑(fderivLM 𝕜 n k) : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F))

Tactic:
continuous_of_isBounded (ContDiffMapSupportedIn.withSeminorms ..)
      (ContDiffMapSupportedIn.withSeminorms ..) _ (fun i ↦ ⟨{i+1}, 1, fun f ↦ ?_⟩)

Premises used: HAdd.hAdd, Exists.intro, WithSeminorms.continuous_of_isBounded, ContDiffMapSupportedIn.withSeminorms, Singleton.singleton, OfNat.ofNat
-- 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
refine :
  ∀ (i : ℕ) (f : 𝓓^{n}_{K}(E, F)),
    LE.le (α := (fun (a : 𝓓^{n}_{K}(E, F)) ↦ ℝ) f)
      ((fun (f : Seminorm 𝕜 𝓓^{n}_{K}(E, F)) ↦ ((⇑f : (a : 𝓓^{n}_{K}(E, F)) → ℝ) : (a : 𝓓^{n}_{K}(E, F)) → ℝ))
        (Seminorm.comp (𝕜₂ := 𝕜) (E₂ := 𝓓^{k}_{K}(E, E →L[ℝ] F)) (σ₁₂ := RingHom.id 𝕜)
          (ContDiffMapSupportedIn.seminorm 𝕜 E (E →L[ℝ] F) k K i) (fderivLM 𝕜 n k))
        f)
      ((fun (f : Seminorm 𝕜 𝓓^{n}_{K}(E, F)) ↦ ((⇑f : (a : 𝓓^{n}_{K}(E, F)) → ℝ) : (a : 𝓓^{n}_{K}(E, F)) → ℝ))
        (HSMul.hSMul (α := ℝ≥0) (β := Seminorm 𝕜 𝓓^{n}_{K}(E, F)) 1
          (Finset.sup {i + 1} (ContDiffMapSupportedIn.seminorm 𝕜 E F n K)))
        f)
⊢ Continuous (X := 𝓓^{n}_{K}(E, F)) (Y := 𝓓^{k}_{K}(E, E →L[ℝ] F))
    (⇑(fderivLM 𝕜 n k) : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F))

Tactic:
refine continuous_of_isBounded (ContDiffMapSupportedIn.withSeminorms ..)
      (ContDiffMapSupportedIn.withSeminorms ..) _ (fun i ↦ ⟨{i+1}, 1, fun f ↦ ?_⟩)

Premises used: HAdd.hAdd, Exists.intro, WithSeminorms.continuous_of_isBounded, ContDiffMapSupportedIn.withSeminorms, Singleton.singleton, OfNat.ofNat
-- 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
i : ℕ
f : 𝓓^{n}_{K}(E, F)
⊢ LE.le (α := (fun (a : 𝓓^{n}_{K}(E, F)) ↦ ℝ) f)
    ((fun (f : Seminorm 𝕜 𝓓^{n}_{K}(E, F)) ↦ ((⇑f : (a : 𝓓^{n}_{K}(E, F)) → ℝ) : (a : 𝓓^{n}_{K}(E, F)) → ℝ))
      (Seminorm.comp (𝕜₂ := 𝕜) (E₂ := 𝓓^{k}_{K}(E, E →L[ℝ] F)) (σ₁₂ := RingHom.id 𝕜)
        (ContDiffMapSupportedIn.seminorm 𝕜 E (E →L[ℝ] F) k K i) (fderivLM 𝕜 n k))
      f)
    ((fun (f : Seminorm 𝕜 𝓓^{n}_{K}(E, F)) ↦ ((⇑f : (a : 𝓓^{n}_{K}(E, F)) → ℝ) : (a : 𝓓^{n}_{K}(E, F)) → ℝ))
      (HSMul.hSMul (α := ℝ≥0) (β := Seminorm 𝕜 𝓓^{n}_{K}(E, F)) 1
        (Finset.sup {i + 1} (ContDiffMapSupportedIn.seminorm 𝕜 E F n K)))
      f)

Tactic:
simpa using seminorm_fderivLM_le 𝕜 f

Premises used: ContDiffMapSupportedIn.seminorm_fderivLM_le
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
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
n k : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
⊢ (⇑((fderivCLM 𝕜 n k : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F)) f : 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
      (a : E) → E →L[ℝ] F) =
    if k + 1 ≤ n then fderiv ℝ (⇑f : (a : E) → F) else 0

Tactic:
fderivLM_apply 𝕜 f

Premises used: ContDiffMapSupportedIn.fderivLM_apply
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
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
n k : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
hk : k + 1 ≤ n
⊢ (⇑((fderivCLM 𝕜 n k : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F)) f : 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
      (a : E) → E →L[ℝ] F) =
    fderiv ℝ (⇑f : (a : E) → F)

Tactic:
fderivLM_apply_of_le 𝕜 f hk

Premises used: ContDiffMapSupportedIn.fderivLM_apply_of_le
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
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
n k : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
hk : n < k + 1
⊢ Eq (α := 𝓓^{k}_{K}(E, E →L[ℝ] F))
    ((fderivCLM 𝕜 n k : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F)) f : 𝓓^{k}_{K}(E, E →L[ℝ] F))
    (0 : 𝓓^{k}_{K}(E, E →L[ℝ] F))

Tactic:
fderivLM_apply_of_gt 𝕜 f hk

Premises used: ContDiffMapSupportedIn.fderivLM_apply_of_gt
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
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
n k : ℕ∞
K : Compacts E
𝕜' : Type u_5
inst_7 : NontriviallyNormedField 𝕜'
inst_8 : NormedSpace 𝕜' F
inst_9 : SMulCommClass ℝ 𝕜' F
⊢ Eq (α := (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F))
    (⇑(fderivCLM 𝕜 n k) : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F))
    (⇑(fderivCLM 𝕜' n k) : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
f : 𝓓^{n}_{K}(E, F)
⊢ StronglyMeasurable (⇑f : (a : E) → F)

Tactic:
f.continuous.stronglyMeasurable_of_hasCompactSupport f.hasCompactSupport

Premises used: Continuous.stronglyMeasurable_of_hasCompactSupport, ContDiffMapSupportedIn.continuous, ContDiffMapSupportedIn.hasCompactSupport
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
f : 𝓓^{n}_{K}(E, F)
⊢ StronglyMeasurable (⇑f : (a : E) → F)

Tactic:
exact f.continuous.stronglyMeasurable_of_hasCompactSupport f.hasCompactSupport

Premises used: Continuous.stronglyMeasurable_of_hasCompactSupport, ContDiffMapSupportedIn.continuous, ContDiffMapSupportedIn.hasCompactSupport
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
μ : Measure E
f : 𝓓^{n}_{K}(E, F)
⊢ AEStronglyMeasurable (⇑f : (a : E) → F) μ

Tactic:
f.stronglyMeasurable.aestronglyMeasurable

Premises used: ContDiffMapSupportedIn.stronglyMeasurable, MeasureTheory.StronglyMeasurable.aestronglyMeasurable
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
μ : Measure E
f : 𝓓^{n}_{K}(E, F)
⊢ MemLp (⇑f : (a : E) → F) ⊤ μ

Tactic:
f.continuous.memLp_top_of_hasCompactSupport f.hasCompactSupport μ

Premises used: ContDiffMapSupportedIn.continuous, ContDiffMapSupportedIn.hasCompactSupport, Continuous.memLp_top_of_hasCompactSupport
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
μ : Measure E
μ_finite : IsFiniteMeasure (μ.restrict (↑K : Set E))
f : 𝓓^{n}_{K}(E, F)
rw : IntegrableOn (⇑f : (a : E) → F) (↑K : Set E) μ
⊢ Integrable (⇑f : (a : E) → F) μ

Tactic:
rw [← integrableOn_iff_integrable_of_support_subset f.support_subset]

Premises used: MeasureTheory.integrableOn_iff_integrable_of_support_subset, ContDiffMapSupportedIn.support_subset
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
μ : Measure E
μ_finite : IsFiniteMeasure (μ.restrict (↑K : Set E))
f : 𝓓^{n}_{K}(E, F)
⊢ IntegrableOn (⇑f : (a : E) → F) (↑K : Set E) μ

Tactic:
f.continuous.integrable_of_hasCompactSupport f.hasCompactSupport

Premises used: ContDiffMapSupportedIn.continuous, Continuous.integrable_of_hasCompactSupport, ContDiffMapSupportedIn.hasCompactSupport, MeasureTheory.IntegrableOn
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
μ : Measure E
μ_finite : IsFiniteMeasure (μ.restrict (↑K : Set E))
f : 𝓓^{n}_{K}(E, F)
⊢ IntegrableOn (⇑f : (a : E) → F) (↑K : Set E) μ

Tactic:
exact f.continuous.integrable_of_hasCompactSupport f.hasCompactSupport

Premises used: ContDiffMapSupportedIn.continuous, Continuous.integrable_of_hasCompactSupport, ContDiffMapSupportedIn.hasCompactSupport
-- 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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K : Set E) μ
f : 𝓓^{n}_{K}(E, F₁)
this :
  IntegrableOn.{u_2, u_7} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x))
    (↑K : Set E) μ
rwa :
  (support.{u_2, u_7} (M := F₃) fun (x : E) ↦
      (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) ⊆
    (↑K : Set E)
⊢ Integrable.{u_7, u_2} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) μ

Tactic:
rwa [integrableOn_iff_integrable_of_support_subset] at this

Premises used: MeasureTheory.integrableOn_iff_integrable_of_support_subset
-- 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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K : Set E) μ
f : 𝓓^{n}_{K}(E, F₁)
this :
  IntegrableOn.{u_2, u_7} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x))
    (↑K : Set E) μ
⊢ (support.{u_2, u_7} (M := F₃) fun (x : E) ↦
      (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) ⊆
    (↑K : Set E)

Tactic:
subset_trans ?_ f.support_subset

Premises used: subset_trans, ContDiffMapSupportedIn.support_subset
-- 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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K : Set E) μ
f : 𝓓^{n}_{K}(E, F₁)
this :
  IntegrableOn.{u_2, u_7} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x))
    (↑K : Set E) μ
refine :
  (support.{u_2, u_7} (M := F₃) fun (x : E) ↦
      (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) ⊆
    support (⇑f : (a : E) → F₁)
⊢ (support.{u_2, u_7} (M := F₃) fun (x : E) ↦
      (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) ⊆
    (↑K : Set E)

Tactic:
refine subset_trans ?_ f.support_subset

Premises used: subset_trans, ContDiffMapSupportedIn.support_subset
-- 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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K : Set E) μ
f : 𝓓^{n}_{K}(E, F₁)
this :
  IntegrableOn.{u_2, u_7} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x))
    (↑K : Set E) μ
x : E
hx :
  Membership.mem (γ := Set E)
    (support.{u_2, u_7} (M := F₃) fun (x : E) ↦
      (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x))
    x
hfx : (f : (a : E) → F₁) x = 0
⊢ Eq.{u_7 + 1} (α := F₃)
    ((fun (x : E) ↦ ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃))
      x)
    0

Tactic:
simp [hfx]
-- 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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K : Set E) μ
f : 𝓓^{n}_{K}(E, F₁)
this :
  IntegrableOn.{u_2, u_7} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x))
    (↑K : Set E) μ
⊢ (support.{u_2, u_7} (M := F₃) fun (x : E) ↦
      (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) ⊆
    support (⇑f : (a : E) → F₁)

Tactic:
exact fun x hx hfx ↦ hx (by simp [hfx])
-- 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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K : Set E) μ
f : 𝓓^{n}_{K}(E, F₁)
suffices :
  IntegrableOn.{u_2, u_7} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x))
    (↑K : Set E) μ
⊢ Integrable.{u_7, u_2} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) μ

Tactic:
suffices IntegrableOn (fun x ↦ B (f x) (φ x)) K μ by
    rwa [integrableOn_iff_integrable_of_support_subset] at this
    refine subset_trans ?_ f.support_subset
    exact fun x hx hfx ↦ hx (by simp [hfx])
-- 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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K : Set E) μ
f : 𝓓^{n}_{K}(E, F₁)
rw :
  ∀ (hφ : MemLp φ 1 (μ.restrict (↑K : Set E))) (f : 𝓓^{n}_{K}(E, F₁)),
    MemLp.{u_2, u_7} (ε := F₃)
      (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) 1
      (μ.restrict (↑K : Set E))
⊢ IntegrableOn.{u_2, u_7} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x))
    (↑K : Set E) μ

Tactic:
rw [IntegrableOn, ← memLp_one_iff_integrable] at hφ ⊢

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.memLp_one_iff_integrable
-- 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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : MemLp φ 1 (μ.restrict (↑K : Set E))
f : 𝓓^{n}_{K}(E, F₁)
⊢ MemLp.{u_2, u_7} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) 1
    (μ.restrict (↑K : Set E))

Tactic:
B.memLp_of_bilin 1 f.memLp_top hφ

Premises used: ContDiffMapSupportedIn.memLp_top, ContinuousLinearMap.memLp_of_bilin, OfNat.ofNat
-- 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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : MemLp φ 1 (μ.restrict (↑K : Set E))
f : 𝓓^{n}_{K}(E, F₁)
⊢ MemLp.{u_2, u_7} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) 1
    (μ.restrict (↑K : Set E))

Tactic:
exact B.memLp_of_bilin 1 f.memLp_top hφ

Premises used: ContDiffMapSupportedIn.memLp_top, ContinuousLinearMap.memLp_of_bilin, OfNat.ofNat
-- 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₁)
pos :
  ∀ (hφ : IntegrableOn φ (↑K : Set E) μ),
    ∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f + g : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ =
      HAdd.hAdd (α := F₃)
        (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
        (∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((g : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ)
neg : ∀ (hφ : ¬IntegrableOn φ (↑K : Set E) μ), 0 = HAdd.hAdd (α := F₃) 0 0
⊢ (if IntegrableOn φ (↑K : Set E) μ then
      ∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f + g : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ
    else 0) =
    HAdd.hAdd (α := 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)
      (if IntegrableOn φ (↑K : Set E) μ then
        ∫ (x : E), (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((g : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) ∂μ
      else 0)

Tactic:
split_ifs with hφ