Support property for the source-normalized weak tilt

The source charge Z/(I-b) is a positive rescaling of the unit phase rotation. Positive rescaling preserves weak (semi)stability and rescales the support estimate by an explicit positive constant. Thus the support property proved for the phase tilt transports to the exact charge appearing in Proposition 14.16.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.sourceTiltLinearCharge {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (b : ℝ) (Zlin : V →ₗ[ℝ] ℂ) : V →ₗ[ℝ] ℂ

The real-linear realization of the exact source charge Z/(I-b).

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.sourceTiltLinearCharge b Zlin = LinearMap.mulLeft ℝ (Complex.I - ↑b)⁻¹ ∘ₗ Zlin

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.sourceTiltLinearCharge_apply {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (b : ℝ) (Zlin : V →ₗ[ℝ] ℂ) (x : V) : (sourceTiltLinearCharge b Zlin) x = Zlin x / (Complex.I - ↑b)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.sourceTiltLinearCharge_eq_scale_phaseTiltLinearCharge {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (b : ℝ) (Zlin : V →ₗ[ℝ] ℂ) (x : V) : (sourceTiltLinearCharge b Zlin) x = ↑(WeakPreStabilityCondition.sourceTiltScale b) * (phaseTiltLinearCharge (WeakPreStabilityCondition.slopeCutPhase b) Zlin) x

theorem CategoryTheory.Triangulated.WeakStabilityCondition.norm_sourceTiltLinearCharge {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (b : ℝ) (Zlin : V →ₗ[ℝ] ℂ) (x : V) : ‖(sourceTiltLinearCharge b Zlin) x‖ = WeakPreStabilityCondition.sourceTiltScale b * ‖Zlin x‖

The exact source normalization scales the norm of the unit phase rotation by sourceTiltScale b.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTilt_hasSupportProperty {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) (Zlin : V →ₗ[ℝ] ℂ) (hcompat : ∀ (x : V), Zlin x = sigma.Z x) (hsupport : sigma.weakStabilityFunctionOnHeart.HasSupportProperty v Zlin) : (sigma.sourceTiltWeakStabilityFunction b).HasSupportProperty v (sourceTiltLinearCharge b Zlin)

Support-property transport for the exact source charge.