Theorems · Theorem · functional analysis

CFC.tendsto_ite_cfc_rpow_sub_one_ite_log

∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A],
  Filter.Tendsto (fun p a => if a ∈ {b | IsStrictlyPositive b} then cfc (fun x => p⁻¹ * (x ^ p - 1)) a else 0)
    (nhdsWithin 0 (Set.Ioi 0)) (nhds fun a => if a ∈ {b | IsStrictlyPositive b} then CFC.log a else 0)

Defined in

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order

Cited by

2 results in Mathlib

Foundations

Depth 319 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CStarAlgebraPartialOrderStarOrderedRing