Documentation

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow

Real powers defined via the continuous functional calculus #

This file defines real powers via the continuous functional calculus (CFC) and builds its API. This allows one to take real powers of matrices, operators, elements of a C⋆-algebra, etc. The square root is also defined via the non-unital CFC.

Main declarations #

Implementation notes #

We define two separate versions CFC.nnrpow and CFC.rpow due to what happens at 0. Since NNReal.rpow 0 0 = 1, this means that this function does not map zero to zero when the exponent is zero, and hence CFC.nnrpow a 0 = 0 whereas CFC.rpow a 0 = 1. Note that the non-unital version only makes sense for nonnegative exponents, and hence we define it such that the exponent is in ℝ≥0.

Notation #

TODO #

@[reducible, inline]
noncomputable abbrev NNReal.nnrpow (a : NNReal) (b : NNReal) :

Taking a nonnegative power of a nonnegative number. This is defined as a standalone definition in order to speed up automation such as cfc_cont_tac.

Equations
  • a.nnrpow b = a ^ b
Instances For
    @[simp]
    theorem NNReal.nnrpow_def (a : NNReal) (b : NNReal) :
    a.nnrpow b = a ^ b
    theorem NNReal.continuous_nnrpow_const (y : NNReal) :
    Continuous fun (x : NNReal) => x.nnrpow y
    noncomputable def CFC.nnrpow {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] (a : A) (y : NNReal) :
    A

    Real powers of operators, based on the non-unital continuous functional calculus.

    Equations
    Instances For
      @[instance 100]

      Enable a ^ y notation for CFC.nnrpow. This is a low-priority instance to make sure it does not take priority over other instances when they are available.

      Equations
      theorem CFC.nnrpow_def {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] {a : A} {y : NNReal} :
      a ^ y = cfcₙ (fun (x : NNReal) => x.nnrpow y) a
      theorem CFC.nnrpow_add {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] {a : A} {x : NNReal} {y : NNReal} (hx : 0 < x) (hy : 0 < y) :
      a ^ (x + y) = a ^ x * a ^ y
      noncomputable def CFC.sqrt {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] (a : A) :
      A

      Square roots of operators, based on the non-unital continuous functional calculus.

      Equations
      Instances For
        noncomputable def CFC.rpow {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] (a : A) (y : ) :
        A

        Real powers of operators, based on the unital continuous functional calculus.

        Equations
        Instances For
          @[instance 100]
          noncomputable instance CFC.instPowReal {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] :

          Enable a ^ y notation for CFC.rpow. This is a low-priority instance to make sure it does not take priority over other instances when they are available (such as Pow ℝ ℝ).

          Equations
          • CFC.instPowReal = { pow := fun (a : A) (y : ) => CFC.rpow a y }
          @[simp]
          theorem CFC.rpow_eq_pow {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] {a : A} {y : } :
          CFC.rpow a y = a ^ y
          @[simp]
          theorem CFC.rpow_nonneg {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] {a : A} {y : } :
          0 a ^ y
          theorem CFC.rpow_def {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] {a : A} {y : } :
          a ^ y = cfc (fun (x : NNReal) => x ^ y) a
          theorem CFC.rpow_one {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] (a : A) (ha : autoParam (0 a) _auto✝) :
          a ^ 1 = a
          @[simp]
          theorem CFC.one_rpow {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] {x : } :
          1 ^ x = 1
          theorem CFC.rpow_zero {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] (a : A) (ha : autoParam (0 a) _auto✝) :
          a ^ 0 = 1
          theorem CFC.zero_rpow {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] {x : } (hx : x 0) :
          CFC.rpow 0 x = 0
          theorem CFC.rpow_natCast {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] (a : A) (n : ) (ha : autoParam (0 a) _auto✝) :
          a ^ n = a ^ n
          @[simp]
          theorem CFC.rpow_algebraMap {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] {x : NNReal} {y : } :
          (algebraMap NNReal A) x ^ y = (algebraMap NNReal A) (x ^ y)
          theorem CFC.rpow_add {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] {a : A} {x : } {y : } (ha : 0spectrum NNReal a) :
          a ^ (x + y) = a ^ x * a ^ y
          theorem CFC.rpow_rpow {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] [UniqueContinuousFunctionalCalculus NNReal A] (a : A) (x : ) (y : ) (ha₁ : 0spectrum NNReal a) (hx : x 0) (ha₂ : autoParam (0 a) _auto✝) :
          (a ^ x) ^ y = a ^ (x * y)
          theorem CFC.rpow_rpow_of_exponent_nonneg {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] [UniqueContinuousFunctionalCalculus NNReal A] (a : A) (x : ) (y : ) (hx : 0 x) (hy : 0 y) (ha₂ : autoParam (0 a) _auto✝) :
          (a ^ x) ^ y = a ^ (x * y)
          theorem CFC.rpow_mul_rpow_neg {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] {a : A} (x : ) (ha : 0spectrum NNReal a) (ha' : autoParam (0 a) _auto✝) :
          a ^ x * a ^ (-x) = 1
          theorem CFC.rpow_neg_mul_rpow {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] {a : A} (x : ) (ha : 0spectrum NNReal a) (ha' : autoParam (0 a) _auto✝) :
          a ^ (-x) * a ^ x = 1
          theorem CFC.rpow_neg_one_eq_inv {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] (a : Aˣ) (ha : autoParam (0 a) _auto✝) :
          a ^ (-1) = a⁻¹
          theorem CFC.rpow_neg {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] [UniqueContinuousFunctionalCalculus NNReal A] (a : Aˣ) (x : ) (ha' : autoParam (0 a) _auto✝) :
          a ^ (-x) = a⁻¹ ^ x
          theorem CFC.rpow_intCast {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] (a : Aˣ) (n : ) (ha : autoParam (0 a) _auto✝) :
          a ^ n = (a ^ n)
          theorem CFC.nnrpow_eq_rpow {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] [∀ (a : A), CompactSpace (spectrum a)] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] {a : A} {x : NNReal} (hx : 0 < x) :
          a ^ x = a ^ x
          theorem CFC.sqrt_rpow_nnreal {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 a] [∀ (a : A), CompactSpace (spectrum a)] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] {a : A} {x : NNReal} :
          CFC.sqrt (a ^ x) = a ^ (x / 2)