OAI/Analysis/KadisonKastler/StrongAnalyticApply.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.tendsto_strong_apply line 19

   Source documentation

   A locally bounded strong operator limit can be evaluated on converging vectors.

   theorem tendsto_strong_apply {l : Filter X} {A : X → E →L[ℂ] F} {A₀ : E →L[ℂ] F}
       (hA : ∀ y, Tendsto (fun s => A s y) l (𝓝 (A₀ y)))
       {B : ℝ} (hB : ∀ᶠ s in l, ‖A s‖ ≤ B)
       {x : X → E} {x₀ : E} (hx : Tendsto x l (𝓝 x₀)) :
       Tendsto (fun s => A s (x s)) l (𝓝 (A₀ x₀)) := by
   …

2. theorem OAI.KadisonKastler.differentiableAt_strong_apply line 36

   Source documentation

   Strong holomorphicity and a local operator bound suffice for the product rule.

   theorem differentiableAt_strong_apply {A : ℂ → E →L[ℂ] F} {z₀ : ℂ}
       (hA : ∀ y, DifferentiableAt ℂ (fun z => A z y) z₀)
       {B : ℝ} (hB : ∀ᶠ z in 𝓝 z₀, ‖A z‖ ≤ B)
       {x : ℂ → E} (hx : DifferentiableAt ℂ x z₀) :
       DifferentiableAt ℂ (fun z => A z (x z)) z₀ := by
   …