Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case hadd
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace ℝ E
inst✝¹⁷ : NormedAddCommGroup F
inst✝¹⁶ : NormedSpace ℝ F
inst✝¹⁵ : NormedSpace 𝕜 F
inst✝¹⁴ : SMulCommClass ℝ 𝕜 F
inst✝¹³ : NormedAddCommGroup F'
inst✝¹² : NormedSpace ℝ F'
inst✝¹¹ : NormedSpace 𝕜 F'
inst✝¹⁰ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
G : Type u_8
inst✝⁹ : NormedAlgebra ℝ 𝕜
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace 𝕜 F₁
inst✝⁶ : NormedSpace ℝ F₁
inst✝⁵ : NormedAddCommGroup F₂
inst✝⁴ : NormedSpace 𝕜 F₂
inst✝³ : NormedSpace ℝ F₂
inst✝² : NormedAddCommGroup F₃
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : NormedSpace ℝ F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
g : E → F₂
hg : ContDiff ℝ (↑n) g
⊢ ∀ (f g_1 : 𝓓^{n}_{K}(E, F₁)) (x : E), (B ((f + g_1) x)) (g x) = (B (f x)) (g x) + (B (g_1 x)) (g x)

pp: case hsmul
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace ℝ E
inst✝¹⁷ : NormedAddCommGroup F
inst✝¹⁶ : NormedSpace ℝ F
inst✝¹⁵ : NormedSpace 𝕜 F
inst✝¹⁴ : SMulCommClass ℝ 𝕜 F
inst✝¹³ : NormedAddCommGroup F'
inst✝¹² : NormedSpace ℝ F'
inst✝¹¹ : NormedSpace 𝕜 F'
inst✝¹⁰ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
G : Type u_8
inst✝⁹ : NormedAlgebra ℝ 𝕜
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace 𝕜 F₁
inst✝⁶ : NormedSpace ℝ F₁
inst✝⁵ : NormedAddCommGroup F₂
inst✝⁴ : NormedSpace 𝕜 F₂
inst✝³ : NormedSpace ℝ F₂
inst✝² : NormedAddCommGroup F₃
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : NormedSpace ℝ F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
g : E → F₂
hg : ContDiff ℝ (↑n) g
⊢ ∀ (c : 𝕜) (f : 𝓓^{n}_{K}(E, F₁)) (x : E), (B ((c • f) x)) (g x) = c • (B (f x)) (g x)

pp: case hsmooth
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace ℝ E
inst✝¹⁷ : NormedAddCommGroup F
inst✝¹⁶ : NormedSpace ℝ F
inst✝¹⁵ : NormedSpace 𝕜 F
inst✝¹⁴ : SMulCommClass ℝ 𝕜 F
inst✝¹³ : NormedAddCommGroup F'
inst✝¹² : NormedSpace ℝ F'
inst✝¹¹ : NormedSpace 𝕜 F'
inst✝¹⁰ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
G : Type u_8
inst✝⁹ : NormedAlgebra ℝ 𝕜
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace 𝕜 F₁
inst✝⁶ : NormedSpace ℝ F₁
inst✝⁵ : NormedAddCommGroup F₂
inst✝⁴ : NormedSpace 𝕜 F₂
inst✝³ : NormedSpace ℝ F₂
inst✝² : NormedAddCommGroup F₃
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : NormedSpace ℝ F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
g : E → F₂
hg : ContDiff ℝ (↑n) g
φ : 𝓓^{n}_{K}(E, F₁)
⊢ ContDiff ℝ ↑n fun x ↦ (B (φ x)) (g x)

pp: case hsupp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace ℝ E
inst✝¹⁷ : NormedAddCommGroup F
inst✝¹⁶ : NormedSpace ℝ F
inst✝¹⁵ : NormedSpace 𝕜 F
inst✝¹⁴ : SMulCommClass ℝ 𝕜 F
inst✝¹³ : NormedAddCommGroup F'
inst✝¹² : NormedSpace ℝ F'
inst✝¹¹ : NormedSpace 𝕜 F'
inst✝¹⁰ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
G : Type u_8
inst✝⁹ : NormedAlgebra ℝ 𝕜
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace 𝕜 F₁
inst✝⁶ : NormedSpace ℝ F₁
inst✝⁵ : NormedAddCommGroup F₂
inst✝⁴ : NormedSpace 𝕜 F₂
inst✝³ : NormedSpace ℝ F₂
inst✝² : NormedAddCommGroup F₃
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : NormedSpace ℝ F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
g : E → F₂
hg : ContDiff ℝ (↑n) g
φ : 𝓓^{n}_{K}(E, F₁)
x : E
hx : x ∈ (↑K)ᶜ
⊢ (fun x ↦ (B (φ x)) (g x)) x = 0 x

pp: case hbound
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace ℝ E
inst✝¹⁷ : NormedAddCommGroup F
inst✝¹⁶ : NormedSpace ℝ F
inst✝¹⁵ : NormedSpace 𝕜 F
inst✝¹⁴ : SMulCommClass ℝ 𝕜 F
inst✝¹³ : NormedAddCommGroup F'
inst✝¹² : NormedSpace ℝ F'
inst✝¹¹ : NormedSpace 𝕜 F'
inst✝¹⁰ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k✝ : ℕ∞
K K₁ K₂ : Compacts E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
G : Type u_8
inst✝⁹ : NormedAlgebra ℝ 𝕜
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace 𝕜 F₁
inst✝⁶ : NormedSpace ℝ F₁
inst✝⁵ : NormedAddCommGroup F₂
inst✝⁴ : NormedSpace 𝕜 F₂
inst✝³ : NormedSpace ℝ F₂
inst✝² : NormedAddCommGroup F₃
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : NormedSpace ℝ F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
g : E → F₂
hg : ContDiff ℝ (↑n) g
k : ℕ
hk : ↑k ≤ n
⊢ ∃ s C,
    0 ≤ C ∧
      ∀ (f : 𝓓^{n}_{K}(E, F₁)),
        ∀ x ∈ K,
          ‖iteratedFDeriv ℝ k (fun x ↦ (B (f x)) (g x)) x‖ ≤
            C * (s.sup fun j ↦ ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K j) f

Tactic:
case hadd | hsmul => intros; simp
  case hsmooth =>
    exact (B.bilinearRestrictScalars ℝ).isBoundedBilinearMap.contDiff.comp (φ.contDiff.prodMk hg)
  case hsupp => simp only [φ.zero_on_compl hx, Pi.zero_apply, map_zero, zero_apply]
  case hbound =>
    have hcont : Continuous fun x ↦ (Finset.range (k + 1)).sup' Finset.nonempty_range_add_one
        (fun i ↦ ‖iteratedFDeriv ℝ i g x‖) :=
      Continuous.finset_sup'_apply Finset.nonempty_range_add_one fun i hi ↦
        (hg.continuous_iteratedFDeriv (WithTop.coe_le_coe.2
          (le_trans (WithTop.coe_le_coe.2 (mem_range_succ_iff.mp hi)) hk))).norm
    obtain ⟨C₀, hC₀⟩ := K.isCompact.exists_bound_of_continuousOn hcont.continuousOn
    have hgC₀ : ∀ i ≤ k, ∀ x ∈ K, ‖iteratedFDeriv ℝ i g x‖ ≤ ‖C₀‖ := fun i hi x hx ↦
      (Finset.le_sup' _ (Finset.mem_range_succ_iff.2 hi)).trans
        ((Real.le_norm_self _).trans ((hC₀ x hx).trans (Real.le_norm_self C₀)))
    refine ⟨Finset.Iic k, ‖B‖ * 2 ^ k * ‖C₀‖, by positivity, fun φ x hx ↦ ?_⟩
    calc
      ‖iteratedFDeriv ℝ k (fun y ↦ B (φ y) (g y)) x‖
        ≤ ‖B‖ * ∑ i ∈ Finset.range (k + 1), (k.choose i : ℝ) * ‖iteratedFDeriv ℝ i φ x‖ *
            ‖iteratedFDeriv ℝ (k - i) g x‖ := by
          simpa using (B.bilinearRestrictScalars ℝ).norm_iteratedFDeriv_le_of_bilinear
            φ.contDiff hg x (mod_cast hk)
      _ ≤ ‖B‖ * ∑ i ∈ Finset.range (k + 1), (k.choose i : ℝ) *
            ((Finset.Iic k).sup fun m ↦ N[𝕜]_{K, n, m}) φ * ‖C₀‖ := by
          gcongr with i hi
          · exact (norm_iteratedFDeriv_apply_le_seminorm 𝕜
              ((WithTop.coe_le_coe.2 (mem_range_succ_iff.mp hi)).trans hk)).trans
              (Seminorm.le_finset_sup_apply (Finset.mem_Iic.2 (mem_range_succ_iff.mp hi)))
          · exact hgC₀ (k - i) (Nat.sub_le k i) x hx
      _ = ‖B‖ * 2 ^ k * ‖C₀‖ * ((Finset.Iic k).sup fun m ↦ N[𝕜]_{K, n, m}) φ := by
          simp_rw [← Finset.sum_mul, ← Nat.cast_sum, Nat.sum_range_choose]
          push_cast
          ring

Goal state after: