14.24. Deformation: TargetEnvelope
14.24.1. phase_confinement_from_stabSeminorm
Phase confinement from the stability seminorm: if E is \operatorname{ssf}-semistable at phase \psi in a thin interval (a, b) with perturbation parameter \varepsilon_0, then \psi - \varepsilon_0 < \varphi^-(E) and \varphi^+(E) < \psi + \varepsilon_0. This is the \operatorname{stabSeminorm}-based wrapper for phase_confinement_of_wSemistable.
Proof: Derive the perturbation bounds from hperturb_of_stabSeminorm, then apply phase_confinement_of_wSemistable.
theorem
CategoryTheory.Triangulated.phase_confinement_from_stabSeminorm.{v, u, u'} (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) (W : Λ →+ ℂ) (hW : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal 1) {E : C} {a b : ℝ} (hab : a < b) {ε₀ : ℝ} (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (hthin : b - a + 2 * ε₀ < 1) (hsin : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε₀))) {ψ : ℝ} (hSS : CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near C σ W hW hab) E ψ) : ψ - ε₀ < CategoryTheory.Triangulated.Slicing.phiMinus C σ.slicing E ⋯ ∧ CategoryTheory.Triangulated.Slicing.phiPlus C σ.slicing E ⋯ < ψ + ε₀CategoryTheory.Triangulated.phase_confinement_from_stabSeminorm.{v, u, u'} (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) (W : Λ →+ ℂ) (hW : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal 1) {E : C} {a b : ℝ} (hab : a < b) {ε₀ : ℝ} (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (hthin : b - a + 2 * ε₀ < 1) (hsin : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε₀))) {ψ : ℝ} (hSS : CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near C σ W hW hab) E ψ) : ψ - ε₀ < CategoryTheory.Triangulated.Slicing.phiMinus C σ.slicing E ⋯ ∧ CategoryTheory.Triangulated.Slicing.phiPlus C σ.slicing E ⋯ < ψ + ε₀
Something wrong, better idea? Suggest a change
14.24.2. gtProp_of_wSemistable_phase_gt
\mathcal{P}(> t) from W-semistability: if E is W-semistable at phase \psi and t < \psi - \varepsilon_0, then E \in \mathcal{P}(> t). Phase confinement gives \varphi^-(E) > \psi - \varepsilon_0 > t.
Proof: Phase confinement gives \varphi^-(E) > \psi - \varepsilon_0 > t, then gtProp_of_phiMinus_gt yields E \in \mathcal{P}(> t).
theorem
CategoryTheory.Triangulated.gtProp_of_wSemistable_phase_gt.{v, u, u'} (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) (W : Λ →+ ℂ) (hW : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal 1) {E : C} {a b : ℝ} (hab : a < b) {ε₀ : ℝ} (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (hthin : b - a + 2 * ε₀ < 1) (hsin : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε₀))) {ψ t : ℝ} (hSS : CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near C σ W hW hab) E ψ) (hgt : t < ψ - ε₀) : CategoryTheory.Triangulated.Slicing.gtProp C σ.slicing t ECategoryTheory.Triangulated.gtProp_of_wSemistable_phase_gt.{v, u, u'} (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) (W : Λ →+ ℂ) (hW : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal 1) {E : C} {a b : ℝ} (hab : a < b) {ε₀ : ℝ} (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (hthin : b - a + 2 * ε₀ < 1) (hsin : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε₀))) {ψ t : ℝ} (hSS : CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near C σ W hW hab) E ψ) (hgt : t < ψ - ε₀) : CategoryTheory.Triangulated.Slicing.gtProp C σ.slicing t E
Something wrong, better idea? Suggest a change
14.24.3. ltProp_of_wSemistable_phase_lt
\mathcal{P}(< t) from W-semistability: if E is W-semistable at phase \psi and \psi + \varepsilon_0 < t, then E \in \mathcal{P}(< t). Phase confinement gives \varphi^+(E) < \psi + \varepsilon_0 < t.
Proof: Phase confinement gives \varphi^+(E) < \psi + \varepsilon_0 < t, then ltProp_of_phiPlus_lt yields E \in \mathcal{P}(< t).
theorem
CategoryTheory.Triangulated.ltProp_of_wSemistable_phase_lt.{v, u, u'} (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) (W : Λ →+ ℂ) (hW : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal 1) {E : C} {a b : ℝ} (hab : a < b) {ε₀ : ℝ} (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (hthin : b - a + 2 * ε₀ < 1) (hsin : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε₀))) {ψ t : ℝ} (hSS : CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near C σ W hW hab) E ψ) (hlt : ψ + ε₀ < t) : CategoryTheory.Triangulated.Slicing.ltProp C σ.slicing t ECategoryTheory.Triangulated.ltProp_of_wSemistable_phase_lt.{v, u, u'} (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) (W : Λ →+ ℂ) (hW : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal 1) {E : C} {a b : ℝ} (hab : a < b) {ε₀ : ℝ} (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (hthin : b - a + 2 * ε₀ < 1) (hsin : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε₀))) {ψ t : ℝ} (hSS : CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near C σ W hW hab) E ψ) (hlt : ψ + ε₀ < t) : CategoryTheory.Triangulated.Slicing.ltProp C σ.slicing t E
Something wrong, better idea? Suggest a change
14.24.4. wPhaseOf_eq_of_semistable_of_target_envelope
W-phase independence across target envelopes: if E is \operatorname{ssf}-semistable at phase \psi in one interval (a_1, b_1), and \psi \in [a_2 + \varepsilon_0, b_2 - \varepsilon_0] for a second thin interval (a_2, b_2), then \operatorname{wPhaseOf}(W(E), (a_2 + b_2)/2) = \psi.
Proof: The branch-cut independence wPhaseOf_indep applies because \psi lies in the overlap of both branch windows. The original phase equation \operatorname{wPhaseOf}(W(E), (a_1 + b_1)/2) = \psi transfers to the new center.
theorem
CategoryTheory.Triangulated.wPhaseOf_eq_of_semistable_of_target_envelope.{v, u, u'} (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) (W : Λ →+ ℂ) (hW : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal 1) {E : C} {a₁ b₁ : ℝ} (hab₁ : a₁ < b₁) {ψ : ℝ} (hSS : CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near C σ W hW hab₁) E ψ) {a₂ b₂ ε₀ : ℝ} (hε₀ : 0 < ε₀) (henv₂_lo : a₂ + ε₀ ≤ ψ) (henv₂_hi : ψ ≤ b₂ - ε₀) (hthin₂ : b₂ - a₂ + 2 * ε₀ < 1) : CategoryTheory.Triangulated.wPhaseOf (W (CategoryTheory.Triangulated.cl C v E)) ((a₂ + b₂) / 2) = ψCategoryTheory.Triangulated.wPhaseOf_eq_of_semistable_of_target_envelope.{v, u, u'} (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) (W : Λ →+ ℂ) (hW : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal 1) {E : C} {a₁ b₁ : ℝ} (hab₁ : a₁ < b₁) {ψ : ℝ} (hSS : CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near C σ W hW hab₁) E ψ) {a₂ b₂ ε₀ : ℝ} (hε₀ : 0 < ε₀) (henv₂_lo : a₂ + ε₀ ≤ ψ) (henv₂_hi : ψ ≤ b₂ - ε₀) (hthin₂ : b₂ - a₂ + 2 * ε₀ < 1) : CategoryTheory.Triangulated.wPhaseOf (W (CategoryTheory.Triangulated.cl C v E)) ((a₂ + b₂) / 2) = ψ
Something wrong, better idea? Suggest a change
14.24.5. semistable_of_target_envelope_triangleTest
Semistability in a target envelope: if E is \operatorname{ssf}-semistable at phase \psi in (a_1, b_1), lies in \mathcal{P}((a_2, b_2)), \psi \in [a_2 + \varepsilon_0, b_2 - \varepsilon_0], and the triangle test holds in (a_2, b_2), then E is semistable in (a_2, b_2) at phase \psi.
Proof: The interval membership and nonzero condition are given. The phase equation follows from wPhaseOf_eq_of_semistable_of_target_envelope. The triangle test is the provided hypothesis.
theorem
CategoryTheory.Triangulated.semistable_of_target_envelope_triangleTest.{v, u, u'} (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) (W : Λ →+ ℂ) (hW : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal 1) {E : C} {a₁ b₁ : ℝ} (hab₁ : a₁ < b₁) {ψ : ℝ} (hSS : CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near C σ W hW hab₁) E ψ) {a₂ b₂ : ℝ} (hab₂ : a₂ < b₂) (hI₂ : CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a₂ b₂ E) {ε₀ : ℝ} (hε₀ : 0 < ε₀) (henv₂_lo : a₂ + ε₀ ≤ ψ) (henv₂_hi : ψ ≤ b₂ - ε₀) (hthin₂ : b₂ - a₂ + 2 * ε₀ < 1) (htri : ∀ ⦃K Q : C⦄ ⦃f₁ : K ⟶ E⦄ ⦃f₂ : E ⟶ Q⦄ ⦃f₃ : Q ⟶ (CategoryTheory.shiftFunctor C 1).obj K⦄, CategoryTheory.Pretriangulated.Triangle.mk f₁ f₂ f₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a₂ b₂ K → CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a₂ b₂ Q → ¬CategoryTheory.Limits.IsZero K → CategoryTheory.Triangulated.wPhaseOf (W (CategoryTheory.Triangulated.cl C v K)) ((a₂ + b₂) / 2) ≤ ψ) : CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near C σ W hW hab₂) E ψCategoryTheory.Triangulated.semistable_of_target_envelope_triangleTest.{v, u, u'} (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) (W : Λ →+ ℂ) (hW : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal 1) {E : C} {a₁ b₁ : ℝ} (hab₁ : a₁ < b₁) {ψ : ℝ} (hSS : CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near C σ W hW hab₁) E ψ) {a₂ b₂ : ℝ} (hab₂ : a₂ < b₂) (hI₂ : CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a₂ b₂ E) {ε₀ : ℝ} (hε₀ : 0 < ε₀) (henv₂_lo : a₂ + ε₀ ≤ ψ) (henv₂_hi : ψ ≤ b₂ - ε₀) (hthin₂ : b₂ - a₂ + 2 * ε₀ < 1) (htri : ∀ ⦃K Q : C⦄ ⦃f₁ : K ⟶ E⦄ ⦃f₂ : E ⟶ Q⦄ ⦃f₃ : Q ⟶ (CategoryTheory.shiftFunctor C 1).obj K⦄, CategoryTheory.Pretriangulated.Triangle.mk f₁ f₂ f₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a₂ b₂ K → CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a₂ b₂ Q → ¬CategoryTheory.Limits.IsZero K → CategoryTheory.Triangulated.wPhaseOf (W (CategoryTheory.Triangulated.cl C v K)) ((a₂ + b₂) / 2) ≤ ψ) : CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near C σ W hW hab₂) E ψ
Something wrong, better idea? Suggest a change
14.24.6. stabSeminorm_lt_cos_of_hsin_hthin
Seminorm comparison: if \|W - Z\|_\sigma < \sin(\pi\varepsilon_0) and b - a + 2\varepsilon_0 < 1, then \|W - Z\|_\sigma < \cos(\pi(b-a)/2). This bridges the sine-based perturbation hypothesis to the cosine-based W \ne 0 condition.
Proof: The inequality \sin(\pi\varepsilon_0) < \cos(\pi(b-a)/2) follows from the complementary angle identity and the thinness condition b - a + 2\varepsilon_0 < 1. Transitivity gives the result.
theorem
CategoryTheory.Triangulated.stabSeminorm_lt_cos_of_hsin_hthin.{v, u, u'} (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) (W : Λ →+ ℂ) {a b ε₀ : ℝ} (hab : a < b) (hε₀ : 0 < ε₀) (hthin : b - a + 2 * ε₀ < 1) (hsin : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε₀))) : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.cos (Real.pi * (b - a) / 2))CategoryTheory.Triangulated.stabSeminorm_lt_cos_of_hsin_hthin.{v, u, u'} (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) (W : Λ →+ ℂ) {a b ε₀ : ℝ} (hab : a < b) (hε₀ : 0 < ε₀) (hthin : b - a + 2 * ε₀ < 1) (hsin : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε₀))) : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.cos (Real.pi * (b - a) / 2))
Something wrong, better idea? Suggest a change
14.24.7. wPhaseOf_eq_of_intervalProp_upper_inclusion
W-phase equality under upper interval inclusion: if E \in \mathcal{P}((a, b_1)) with b_1 \le b_2 and the thinness condition holds for (a, b_2), then \operatorname{wPhaseOf}(W(E), (a+b_1)/2) = \operatorname{wPhaseOf}(W(E), (a+b_2)/2).
Proof: Derive perturbation bounds for the narrower interval (a, b_1), show the W-phase lies in the overlap of both branch windows, then apply wPhaseOf_indep.
theorem
CategoryTheory.Triangulated.wPhaseOf_eq_of_intervalProp_upper_inclusion.{v, u, u'} (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) (W : Λ →+ ℂ) (hW : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal 1) {a b₁ b₂ ε₀ : ℝ} (hab₁ : a < b₁) (hb : b₁ ≤ b₂) {E : C} (hI : CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b₁ E) (hEne : ¬CategoryTheory.Limits.IsZero E) (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (hthin₂ : b₂ - a + 2 * ε₀ < 1) (hsin : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε₀))) : CategoryTheory.Triangulated.wPhaseOf (W (CategoryTheory.Triangulated.cl C v E)) ((a + b₁) / 2) = CategoryTheory.Triangulated.wPhaseOf (W (CategoryTheory.Triangulated.cl C v E)) ((a + b₂) / 2)CategoryTheory.Triangulated.wPhaseOf_eq_of_intervalProp_upper_inclusion.{v, u, u'} (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) (W : Λ →+ ℂ) (hW : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal 1) {a b₁ b₂ ε₀ : ℝ} (hab₁ : a < b₁) (hb : b₁ ≤ b₂) {E : C} (hI : CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b₁ E) (hEne : ¬CategoryTheory.Limits.IsZero E) (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (hthin₂ : b₂ - a + 2 * ε₀ < 1) (hsin : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε₀))) : CategoryTheory.Triangulated.wPhaseOf (W (CategoryTheory.Triangulated.cl C v E)) ((a + b₁) / 2) = CategoryTheory.Triangulated.wPhaseOf (W (CategoryTheory.Triangulated.cl C v E)) ((a + b₂) / 2)
Something wrong, better idea? Suggest a change
14.24.8. wPhaseOf_eq_of_intervalProp_lower_inclusion
W-phase equality under lower interval inclusion: if E \in \mathcal{P}((a_1, b)) with a_2 \le a_1 and the thinness condition holds for (a_2, b), then \operatorname{wPhaseOf}(W(E), (a_1+b)/2) = \operatorname{wPhaseOf}(W(E), (a_2+b)/2).
Proof: Symmetric to wPhaseOf_eq_of_intervalProp_upper_inclusion: derive perturbation bounds for the narrower interval, verify branch-window overlap, apply wPhaseOf_indep.
theorem
CategoryTheory.Triangulated.wPhaseOf_eq_of_intervalProp_lower_inclusion.{v, u, u'} (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) (W : Λ →+ ℂ) (hW : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal 1) {a₁ a₂ b ε₀ : ℝ} (ha₁ : a₁ < b) (ha : a₂ ≤ a₁) {E : C} (hI : CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a₁ b E) (hEne : ¬CategoryTheory.Limits.IsZero E) (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (hthin₂ : b - a₂ + 2 * ε₀ < 1) (hsin : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε₀))) : CategoryTheory.Triangulated.wPhaseOf (W (CategoryTheory.Triangulated.cl C v E)) ((a₁ + b) / 2) = CategoryTheory.Triangulated.wPhaseOf (W (CategoryTheory.Triangulated.cl C v E)) ((a₂ + b) / 2)CategoryTheory.Triangulated.wPhaseOf_eq_of_intervalProp_lower_inclusion.{v, u, u'} (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) (W : Λ →+ ℂ) (hW : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal 1) {a₁ a₂ b ε₀ : ℝ} (ha₁ : a₁ < b) (ha : a₂ ≤ a₁) {E : C} (hI : CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a₁ b E) (hEne : ¬CategoryTheory.Limits.IsZero E) (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (hthin₂ : b - a₂ + 2 * ε₀ < 1) (hsin : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε₀))) : CategoryTheory.Triangulated.wPhaseOf (W (CategoryTheory.Triangulated.cl C v E)) ((a₁ + b) / 2) = CategoryTheory.Triangulated.wPhaseOf (W (CategoryTheory.Triangulated.cl C v E)) ((a₂ + b) / 2)
Something wrong, better idea? Suggest a change
14.24.9. wPhaseOf_mem_Ioo_of_intervalProp_target_envelope
For E \in \mathcal{P}((a, b)) nonzero, the W-phase at center (a+b)/2 lies in the open interval (\psi - 1, \psi + 1) whenever \psi \in [a + \varepsilon_0, b - \varepsilon_0]. This is the branch-cut membership needed for wPhaseOf_indep.
Proof: The global perturbation bounds give a - \varepsilon_0 < \operatorname{wPhaseOf}(W(E), (a+b)/2) < b + \varepsilon_0. Since \psi \in [a + \varepsilon_0, b - \varepsilon_0] and b - a + 2\varepsilon_0 < 1, both \psi - 1 and \psi + 1 are outside the W-phase range, giving strict containment.
theorem
CategoryTheory.Triangulated.wPhaseOf_mem_Ioo_of_intervalProp_target_envelope.{v, u, u'} (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) (W : Λ →+ ℂ) (hW : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal 1) {a b ψ ε₀ : ℝ} {E : C} (hI : CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b E) (hEne : ¬CategoryTheory.Limits.IsZero E) (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (henv_lo : a + ε₀ ≤ ψ) (henv_hi : ψ ≤ b - ε₀) (hthin : b - a + 2 * ε₀ < 1) (hsin : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε₀))) : CategoryTheory.Triangulated.wPhaseOf (W (CategoryTheory.Triangulated.cl C v E)) ((a + b) / 2) ∈ Set.Ioo (ψ - 1) (ψ + 1)CategoryTheory.Triangulated.wPhaseOf_mem_Ioo_of_intervalProp_target_envelope.{v, u, u'} (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) (W : Λ →+ ℂ) (hW : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal 1) {a b ψ ε₀ : ℝ} {E : C} (hI : CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b E) (hEne : ¬CategoryTheory.Limits.IsZero E) (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (henv_lo : a + ε₀ ≤ ψ) (henv_hi : ψ ≤ b - ε₀) (hthin : b - a + 2 * ε₀ < 1) (hsin : CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε₀))) : CategoryTheory.Triangulated.wPhaseOf (W (CategoryTheory.Triangulated.cl C v E)) ((a + b) / 2) ∈ Set.Ioo (ψ - 1) (ψ + 1)
Something wrong, better idea? Suggest a change