Common midpoint hearts for nearby phase windows

Two objects centred at nearby phases lie in one shifted owner heart. This is the geometric preparation for factoring a morphism between deformed-slice objects in the small-gap case.

theorem CategoryTheory.Triangulated.midpoint_left_target_thin {ψ₁ ψ₂ ε : ℝ} (hsmall : ψ₁ ≤ ψ₂ + 2 * ε) (hε8 : ε < 1 / 8) : ψ₁ + ε - ((ψ₁ + ψ₂) / 2 - 1 / 2) + 2 * ε < 1

The left target interval around two nearby phases has deformed width less than one.

theorem CategoryTheory.Triangulated.midpoint_right_target_thin {ψ₁ ψ₂ ε : ℝ} (hsmall : ψ₁ ≤ ψ₂ + 2 * ε) (hε8 : ε < 1 / 8) : (ψ₁ + ψ₂) / 2 - 1 / 2 + 1 - (ψ₂ - ε) + 2 * ε < 1

The right target interval around two nearby phases has deformed width less than one.

theorem CategoryTheory.Triangulated.midpoint_image_window_thin {ψ₁ ψ₂ ε : ℝ} (hgap : ψ₂ < ψ₁) (hsmall : ψ₁ ≤ ψ₂ + 2 * ε) (hε8 : ε < 1 / 8) : ψ₂ + ε - (ψ₁ - ε) + 2 * ε < 1

The image window between two ordered nearby phases remains thin.

theorem CategoryTheory.Triangulated.Slicing.mem_phaseShiftHeart_of_midpoint_left (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) {E : C} (hE : ¬Limits.IsZero E) {ψ₁ ψ₂ ε : ℝ} (hlo : ψ₁ - ε ≤ phiMinus C s E hE) (hhi : phiPlus C s E hE ≤ ψ₁ + ε) (hgap : ψ₂ < ψ₁) (hsmall : ψ₁ ≤ ψ₂ + 2 * ε) (hε4 : ε < 1 / 4) : (toTStructure C (phaseShift C s ((ψ₁ + ψ₂) / 2 - 1 / 2))).heart E

An object intrinsically confined around the larger phase lies in the common midpoint heart.

theorem CategoryTheory.Triangulated.Slicing.mem_phaseShiftHeart_of_midpoint_right (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) {E : C} (hE : ¬Limits.IsZero E) {ψ₁ ψ₂ ε : ℝ} (hlo : ψ₂ - ε ≤ phiMinus C s E hE) (hhi : phiPlus C s E hE ≤ ψ₂ + ε) (hgap : ψ₂ < ψ₁) (hsmall : ψ₁ ≤ ψ₂ + 2 * ε) (hε4 : ε < 1 / 4) : (toTStructure C (phaseShift C s ((ψ₁ + ψ₂) / 2 - 1 / 2))).heart E

An object intrinsically confined around the smaller phase lies in the same common midpoint heart.