Documentation

DerivedAlgGeo.CategoryTheory.Triangulated.StabilityCondition.Foundation.Deformation.PhaseArithmetic

Relative-phase arithmetic #

This module develops the rotated imaginary-part calculations behind the phase see-saw argument. It is purely analytic: later categorical deformation modules can use these results through the repository-owned foundation.

source
noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.rotatedIm (w : ℂ) (ψ : ℝ) :
ℝ

The imaginary part of a complex number after rotating phase ψ to the real axis.

Equations
Instances For
    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.rotatedIm_polar (m φ ψ : ℝ) :
    rotatedIm (↑m * Complex.exp (↑(Real.pi * φ) * Complex.I)) ψ = m * Real.sin (Real.pi * (φ - ψ))

    Rotating a polar vector subtracts its phases inside the sine.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.rotatedIm_eq_norm_mul_sin (w : ℂ) (α ψ : ℝ) :
    rotatedIm w ψ = ‖w‖ * Real.sin (Real.pi * (relativePhase w α - ψ))

    Rotated imaginary part expressed through the selected relative phase.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.rotatedIm_eq_zero_of_relativePhase_eq {w : ℂ} {α ψ : ℝ} (h : relativePhase w α = ψ) :
    rotatedIm w ψ = 0

    A vector has zero rotated imaginary part at its selected phase.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.rotatedIm_neg_of_relativePhase_lt {w : ℂ} {α ψ : ℝ} (hw : w ≠ 0) (hlo : ψ - 1 < relativePhase w α) (hlt : relativePhase w α < ψ) :
    rotatedIm w ψ < 0

    A nonzero vector whose selected phase lies strictly below the rotation phase by less than one has negative rotated imaginary part.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.rotatedIm_pos_of_relativePhase_gt {w : ℂ} {α ψ : ℝ} (hw : w ≠ 0) (hgt : ψ < relativePhase w α) (hhi : relativePhase w α < ψ + 1) :
    0 < rotatedIm w ψ

    A nonzero vector whose selected phase lies strictly above the rotation phase by less than one has positive rotated imaginary part.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.relativePhase_gt_of_rotatedIm_pos {w : ℂ} {α ψ : ℝ} (him : 0 < rotatedIm w ψ) (hrange : relativePhase w α ∈ Set.Ioo (ψ - 1) (ψ + 1)) :
    ψ < relativePhase w α

    Positive rotated imaginary part forces a relative phase above the rotation phase, provided the selected branch does not wrap around it.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.relativePhase_lt_of_rotatedIm_neg {w : ℂ} {α ψ : ℝ} (him : rotatedIm w ψ < 0) (hrange : relativePhase w α ∈ Set.Ioo (ψ - 1) (ψ + 1)) :
    relativePhase w α < ψ

    Negative rotated imaginary part forces a relative phase below the rotation phase on the same branch window.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.relativePhase_seesaw {w w₁ w₂ : ℂ} {α ψ : ℝ} (hsum : w₁ + w₂ = w) (hψ : relativePhase w α = ψ) (hw₁_range : relativePhase w₁ α ∈ Set.Ioc (ψ - 1) ψ) (hw₂_ne : w₂ ≠ 0) (hw₂_range : relativePhase w₂ α ∈ Set.Ioo (ψ - 1) (ψ + 1)) :
    ψ ≤ relativePhase w₂ α

    Phase see-saw: if a total vector has phase ψ and the first summand is at most ψ, then a nonzero second summand on the same branch is at least ψ.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.relativePhase_seesaw_strict {w w₁ w₂ : ℂ} {α ψ : ℝ} (hsum : w₁ + w₂ = w) (hψ : relativePhase w α = ψ) (hw₂_lt : relativePhase w₂ α < ψ) (hw₂_ne : w₂ ≠ 0) (hw₂_range : relativePhase w₂ α ∈ Set.Ioo (ψ - 1) (ψ + 1)) (hw₁_range : relativePhase w₁ α ∈ Set.Ioo (ψ - 1) (ψ + 1)) :
    ψ < relativePhase w₁ α

    Strict phase see-saw: a below-phase nonzero second summand forces the first summand strictly above the phase of the total.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.relativePhase_seesaw_dual {w w₁ w₂ : ℂ} {α ψ : ℝ} (hsum : w₁ + w₂ = w) (hψ : relativePhase w α = ψ) (hw₁_gt : ψ < relativePhase w₁ α) (hw₁_ne : w₁ ≠ 0) (hw₁_range : relativePhase w₁ α ∈ Set.Ioo (ψ - 1) (ψ + 1)) (hw₂_range : relativePhase w₂ α ∈ Set.Ioo (ψ - 1) (ψ + 1)) :
    relativePhase w₂ α < ψ

    Dual strict phase see-saw: an above-phase nonzero first summand forces the second summand strictly below the phase of the total.