TraceCalculus.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.KervaireTraceCalculus.hasDerivAt_trace_pow line 24

Source documentation

The derivative of a trace of a noncommutative power has its usual scalar form.

theorem hasDerivAt_trace_pow (τ : E →L[𝕜] F)
    (hτ : ∀ a b : E, τ (a * b) = τ (b * a))
    {f : 𝕜 → E} {f' : E} {x : 𝕜} (hf : HasDerivAt f f' x) (n : ℕ) :
    HasDerivAt (fun y => τ (f y ^ n)) (n • τ (f x ^ (n - 1) * f')) x := by
…

theorem OAI.KervaireTraceCalculus.hasDerivAt_trace_exp_path_pow line 46

Source documentation

Differentiation along the exponential unitary path, before imposing positivity.

theorem hasDerivAt_trace_exp_path_pow (τ : B →L[ℂ] ℂ)
    (hτ : ∀ a b : B, τ (a * b) = τ (b * a)) (U C : B) (z : ℂ) (n : ℕ) :
    HasDerivAt (fun y : ℂ => τ ((U * NormedSpace.exp (y • C)) ^ n))
      ((n : ℂ) * τ ((U * NormedSpace.exp (z • C)) ^ n * C)) z := by
…

theorem OAI.KervaireTraceCalculus.trace_mul_nonneg line 74

Source documentation

Tracial positivity applies to a product of positive elements even when they do not commute.

theorem trace_mul_nonneg (τ : A →L[ℂ] ℂ)
    (ht : ∀ X Y : A, τ (X * Y) = τ (Y * X))
    (hp : ∀ X : A, 0 ≤ (τ (star X * X)).re)
    {B D : A} (hB : 0 ≤ B) (hD : 0 ≤ D) : 0 ≤ (τ (D * B)).re := by
…

theorem OAI.KervaireTraceCalculus.trace_mul_le line 95

Source documentation

The polynomial phase derivative is bounded using positivity, not commutativity between the path generator and the functional calculus.

theorem trace_mul_le (τ : A →L[ℂ] ℂ)
    (ht : ∀ X Y : A, τ (X * Y) = τ (Y * X))
    (hp : ∀ X : A, 0 ≤ (τ (star X * X)).re)
    {B C : A} (hB : 0 ≤ B) {r : ℝ} (hC : C ≤ r • (1 : A)) :
    (τ (C * B)).re ≤ r * (τ B).re := by
…

theorem OAI.KervaireTraceCalculus.hasDerivAt_trace_real_exp_path_pow line 111

Source documentation

The same tracial differentiation formula for a real time parameter.

theorem hasDerivAt_trace_real_exp_path_pow (τ : A →L[ℂ] ℂ)
    (hτ : ∀ a b : A, τ (a * b) = τ (b * a)) (U C : A) (t : ℝ) (n : ℕ) :
    HasDerivAt (fun y : ℝ => τ ((U * NormedSpace.exp (y • C)) ^ n))
      ((n : ℂ) * τ ((U * NormedSpace.exp (t • C)) ^ n * C)) t := by
…

def OAI.KervaireTraceCalculus.traceLog line 131
Source documentation
A regularized logarithm evaluated by a trace.
```
def traceLog (τ : A →L[ℂ] ℂ) (a : ℂ) (U : A) : ℂ :=
…
```
theorem OAI.KervaireTraceCalculus.norm_log_coeff_le line 134
theorem OAI.KervaireTraceCalculus.summable_traceLog line 143
theorem OAI.KervaireTraceCalculus.norm_trace_pow_mul_le line 161

theorem OAI.KervaireTraceCalculus.hasDerivAt_traceLog_path line 174

Source documentation

Uniform geometric bounds justify differentiating the regularized trace. Only real time is needed, so the unitary path is uniformly bounded.

theorem hasDerivAt_traceLog_path [NormOneClass A] (τ : A →L[ℂ] ℂ)
    (hτ : ∀ a b : A, τ (a * b) = τ (b * a)) (U C : A)
    (hb : ∀ t : ℝ, ‖U * NormedSpace.exp (t • C)‖ ≤ 1)
    {a : ℂ} (ha : ‖a‖ < 1) (t : ℝ) :
    HasDerivAt (fun t : ℝ => traceLog τ a (U * NormedSpace.exp (t • C)))
      (∑' n : ℕ, a ^ (n + 1) * τ ((U * NormedSpace.exp (t • C)) ^ (n + 1) * C)) t := by
…

Mentions: OAI.KervaireTraceCalculus.traceLog

theorem OAI.KervaireTraceCalculus.geometricPart_realpart_nonneg line 209
Source documentation
The Hermitian part of the Cayley transform is nonnegative. This algebraic Neumann-series argument is valid in every C-star algebra, not just matrices.
```
theorem geometricPart_realpart_nonneg (Z : A) (hZ : ‖Z‖ < 1) :
    0 ≤ 1 + (∑' n : ℕ, Z ^ (n+1)) + star (∑' n : ℕ, Z ^ (n+1)) := by
…
```

theorem OAI.KervaireTraceCalculus.geometricPart_trace_bound line 234

Source documentation

The Cayley positivity gives the exact one-sided phase derivative bound.

theorem geometricPart_trace_bound (τ : A →L[ℂ] ℂ)
    (ht : ∀ X Y : A, τ (X * Y) = τ (Y * X))
    (hp : ∀ X : A, 0 ≤ (τ (star X * X)).re)
    (hs : ∀ X : A, τ (star X) = star (τ X))
    {B : A} (hB : 0 ≤ B) (Z : A) (hZ : ‖Z‖ < 1) :
    -2 * (τ ((∑' n : ℕ, Z ^ (n+1)) * B)).re ≤ (τ B).re := by
…

theorem OAI.KervaireTraceCalculus.trace_deriv_series line 260

Source documentation

Summing the derivative of the logarithm produces the Cayley series inside the algebra.

theorem trace_deriv_series (τ : A →L[ℂ] ℂ) {a : ℂ} {W : A} (C : A)
    (haW : ‖a • W‖ < 1) :
    (∑' n : ℕ, a ^ (n+1) * τ (W ^ (n+1) * C)) =
      τ ((∑' n : ℕ, (a • W) ^ (n+1)) * C) := by
…

def OAI.KervaireTraceCalculus.phaseVelocity line 272
Source documentation
The derivative generator has the normalization used for fractional phase.
```
def phaseVelocity (B : A) : A := ((2 * Real.pi : ℂ) * Complex.I) • B
…
```
theorem OAI.KervaireTraceCalculus.exp_phaseVelocity_mem_unitary line 276
Source documentation
Positive generators give a unitary path at all real times.
```
theorem exp_phaseVelocity_mem_unitary {B : A} (hB : 0 ≤ B) (t : ℝ) :
    NormedSpace.exp (t • phaseVelocity B) ∈ unitary A := by
…
```
Mentions: OAI.KervaireTraceCalculus.phaseVelocity
def OAI.KervaireTraceCalculus.smoothTrace line 284
Source documentation
A smooth trace approximation to the fractional spectral phase.
```
def smoothTrace (τ : A →L[ℂ] ℂ) (a : ℂ) (U : A) : ℝ :=
…
```

theorem OAI.KervaireTraceCalculus.hasDerivAt_smoothTrace_path line 288

Source documentation

The exact derivative of the regularized phase along a positive path.

theorem hasDerivAt_smoothTrace_path (τ : A →L[ℂ] ℂ)
    (ht : ∀ X Y : A, τ (X * Y) = τ (Y * X))
    {U B : A} (hU : U ∈ unitary A) (hB : 0 ≤ B)
    {a : ℂ} (ha : ‖a‖ < 1) (t : ℝ) :
    HasDerivAt (fun t : ℝ => smoothTrace τ a
      (U * NormedSpace.exp (t • phaseVelocity B)))
      (-2 * (τ ((∑' n : ℕ, (a • (U * NormedSpace.exp
        (t • phaseVelocity B))) ^ (n+1)) * B)).re) t := by
…

Mentions: OAI.KervaireTraceCalculus.smoothTrace, OAI.KervaireTraceCalculus.phaseVelocity

theorem OAI.KervaireTraceCalculus.deriv_smoothTrace_path_le line 317

Source documentation

The one-sided derivative estimate for the smooth regularization.

theorem deriv_smoothTrace_path_le (τ : A →L[ℂ] ℂ)
    (ht : ∀ X Y : A, τ (X * Y) = τ (Y * X))
    (hp : ∀ X : A, 0 ≤ (τ (star X * X)).re)
    (hs : ∀ X : A, τ (star X) = star (τ X))
    {U B : A} (hU : U ∈ unitary A) (hB : 0 ≤ B)
    {a : ℂ} (ha : ‖a‖ < 1) (t : ℝ) :
    deriv (fun t : ℝ => smoothTrace τ a
      (U * NormedSpace.exp (t • phaseVelocity B))) t ≤ (τ B).re := by
…

Mentions: OAI.KervaireTraceCalculus.smoothTrace, OAI.KervaireTraceCalculus.phaseVelocity

theorem OAI.KervaireTraceCalculus.smoothTrace_mul_exp_le line 332

Source documentation

Integrating the regularized derivative bound over the unit path.

theorem smoothTrace_mul_exp_le (τ : A →L[ℂ] ℂ)
    (ht : ∀ X Y : A, τ (X * Y) = τ (Y * X))
    (hp : ∀ X : A, 0 ≤ (τ (star X * X)).re)
    (hs : ∀ X : A, τ (star X) = star (τ X))
    {U B : A} (hU : U ∈ unitary A) (hB : 0 ≤ B)
    {a : ℂ} (ha : ‖a‖ < 1) :
    smoothTrace τ a (U * NormedSpace.exp (phaseVelocity B)) ≤
      smoothTrace τ a U + (τ B).re := by
…

Mentions: OAI.KervaireTraceCalculus.smoothTrace, OAI.KervaireTraceCalculus.phaseVelocity