QIQTH.StandardSubspaceModular
← all sections · ← SpectralTheorem · StandardSubspaceModularFlow →
StandardSubspaceModular · entries 753–807 of 1000
Definition 753 (projK). source ↗
RvD P — the real-orthogonal projection onto the standard subspace 𝒦.
Used by oneParticleBW_niceWedge, h1_of_stripKMSrvd, comparisonDatum_of_gConstancy, gConstancy_of_inputs, oneParticleBW_of_inputs, oneParticleBW_of_stripKMSrvd_density, oneParticleBW_complete, oneParticleBW_wedge_complete, and 51 more.
Definition 754 (projIK). source ↗
RvD Q — the real-orthogonal projection onto i𝒦 = mulI 𝒦.
Used by ComparisonDatum, oneParticleBW_of_comparison, comparisonDatum_of_gConstancy, modUnitary_eq_of_orbit_compare, rvdR, projIK_idem, rvdR_apply, rvdR_inner_self, and 28 more.
Definition 755 (rvdR). source ↗
RvD R = P + Q (Definition 2.1).
Used by rvdR_apply, rvdR_inner_self, rvdR_inner_self_nonneg, rvdR_inner_self_le, rvdR_inner_symm, rvdR_eq_zero, rvdR_smul_I, rvdR_smul_complex, and 23 more.
Lemma 756 (projK_idem). source ↗
P is idempotent (a projection).
Proof. Immediate from the definitions.
Used by rvdRC_mul_rvdTwoSubRC_apply, rvdPmQ_mul_rvdR, rvdSqrtR_range_dense_in_K.
Lemma 757 (projIK_idem). source ↗
Q is idempotent (a projection).
Proof. Immediate from the definitions.
Used by rvdRC_mul_rvdTwoSubRC_apply, rvdPmQ_mul_rvdR, eq_of_mem_K_of_inner_perp_IK.
Lemma 758 (rvdR_apply). source ↗
Proof. Immediate from the definitions.
Used by rvdR_inner_self, rvdR_smul_I, rvdPmQ_eq_zero, modConj_projIK_modConj, modConj_projK_modConj.
Lemma 759 (rvdR_inner_self). source ↗
RvD Prop 2.2(1), key identity: ⟪R ξ, ξ⟫ = ‖P ξ‖² + ‖Q ξ‖². (Each projection is self-adjoint idempotent, so ⟪P ξ, ξ⟫ = ‖P ξ‖².) This is the quadratic form whose vanishing forces P ξ = Q ξ = 0, the crux of R’s injectivity and hence of the well-definedness of the modular operator.
Proof. By rvdR_apply.
Used by rvdR_inner_self_nonneg, rvdR_inner_self_le, rvdR_eq_zero.
Lemma 760 (rvdR_inner_self_nonneg). source ↗
0 ≤ ⟪R ξ, ξ⟫ — the lower half of RvD’s 0 ≤ R ≤ 2.
Proof. By projK, projIK, rvdR_inner_self.
Used by rvdRC_isPositive.
Lemma 761 (norm_projK_apply_le). source ↗
P is a contraction: ‖P ξ‖ ≤ ‖ξ‖.
Proof. Immediate from the definitions.
Used by rvdR_inner_self_le.
Lemma 762 (norm_projIK_apply_le). source ↗
Q is a contraction: ‖Q ξ‖ ≤ ‖ξ‖.
Proof. Immediate from the definitions.
Used by rvdR_inner_self_le.
Lemma 763 (rvdR_inner_self_le). source ↗
⟪R ξ, ξ⟫ ≤ 2‖ξ‖² — the upper half of RvD’s 0 ≤ R ≤ 2 (each projection is a contraction, so ‖P ξ‖² + ‖Q ξ‖² ≤ 2‖ξ‖²).
Proof. By projK, projIK, rvdR_inner_self, norm_projK_apply_le, norm_projIK_apply_le.
Used by rvdR_le_two.
Lemma 764 (rvdR_inner_symm). source ↗
R is symmetric (self-adjoint in the inner-product sense): ⟪R x, y⟫ = ⟪x, R y⟫. Each projection P, Q is self-adjoint (inner_starProjection_left_eq_right). (The stronger operator-level statement IsSelfAdjoint (rvdR S) — star R = R — is rvdR_isSelfAdjoint below, available now that open ClosedSubmodule supplies InnerProductSpace ℝ H and hence the adjoint/Star on H →L[ℝ] H.)
Proof. Immediate from the definitions.
Used by rvdRC_isSymmetric, rvdR_le_two.
Lemma 765 (rvdR_eq_zero). source ↗
RvD Prop 2.2(1): R is injective. If R ξ = 0 then ⟪R ξ, ξ⟫ = 0, so by rvdR_inner_self both ‖P ξ‖ = ‖Q ξ‖ = 0; hence ξ ⊥ 𝒦 and ξ ⊥ i𝒦, i.e. ξ ∈ 𝒦ᗮ ⊓ (i𝒦)ᗮ = (𝒦 ⊔ i𝒦)ᗮ = ⊤ᗮ = ⊥ using S.IsCyclic (𝒦 + i𝒦 dense). Injectivity of R is what makes the modular operator well-defined.
Proof. By projK, projIK, rvdR_inner_self.
Used by rvdPmQ_eq_zero.
Lemma 766 (projK_isSelfAdjoint). source ↗
P is self-adjoint as a bounded operator (star (projK S) = projK S).
Proof. Immediate from the definitions.
Used by rvdPmQ_isSelfAdjoint.
Lemma 767 (projIK_isSelfAdjoint). source ↗
Q is self-adjoint as a bounded operator.
Proof. Immediate from the definitions.
Used by rvdPmQ_isSelfAdjoint, inner_real_of_mem_K_perp_IK.
Lemma 768 (projIK_smul_I). source ↗
Conjugation identity (1): Q(i·ξ) = i·(P ξ) (projIK = J·projK·J⁻¹, J = mult-by-i). Proved by the variational characterization: i·(P ξ) ∈ i𝒦, and i·ξ − i·(P ξ) = i·(ξ − P ξ) is ⊥ᵣ i𝒦 because mult-by-i is an isometry and ξ − P ξ ⊥ᵣ 𝒦.
Proof. Immediate from the definitions.
Used by projK_smul_I, rvdR_smul_I, rvdPmQ_smul_I, modConj_smul_I, inner_real_of_mem_K_perp_IK.
Lemma 769 (projK_smul_I). source ↗
Conjugation identity (2): P(i·ξ) = i·(Q ξ). Algebraic consequence of (1) (projIK_smul_I) via i·(i··) = −·.
Proof. By projIK_smul_I.
Used by rvdR_smul_I, rvdPmQ_smul_I, modConj_smul_I.
Lemma 770 (rvdR_smul_I). source ↗
R = P + Q is ℂ-linear: R(i·ξ) = i·(R ξ). Combines the two conjugation identities; this is exactly the commutation with mult-by-i that lets R be viewed as a complex-linear operator Rℂ : H →L[ℂ] H, on which the complex continuous functional calculus (CFC.sqrt) applies.
Proof. By projK, projIK, rvdR_apply, projIK_smul_I, projK_smul_I.
Used by rvdR_smul_complex, rvdRC_isSymmetric.
Lemma 771 (clm_eq_of_eqOn_K). source ↗
Operator equality from equality on 𝒦 (RvD Theorem 3.8 capstone): two continuous ℂ-linear operators that agree on the standard subspace 𝒦 agree everywhere. By ℂ-linearity they then agree on i𝒦 (q ∈ i𝒦 ⟹ −i·q ∈ 𝒦), hence on the algebraic sum 𝒦 + i𝒦, which is dense (IsCyclic, 𝒦 ⊔ i𝒦 = ⊤); continuity finishes. This lifts the per-vector identity V_t η = Δ^{it} η on 𝒦 (from eq_of_mem_K_of_inner_perp_IK) to the operator identity V_t = Δ^{it} discharging hUniq.
Proof. Immediate from the definitions.
Used by modUnitary_eq_of_orbit_compare.
Lemma 772 (rvdR_smul_complex). source ↗
Full ℂ-map_smul for R: R(c·x) = c·(R x) for every c : ℂ. Decompose c = c.re + c.im·i; the real part uses ℝ-linearity, the imaginary part rvdR_smul_I.
Proof. By rvdR_smul_I.
Used by rvdRC.
Definition 773 (rvdRC). source ↗
R = P + Q as a genuine ℂ-linear continuous operator (same underlying map as rvdR S).
Used by borelFC_congr_ae, deviceOpC_neg_half_eq, rvdSpecMeasure, devSpecReal, devSpecReal_measurable, devSpecReal_norm_le, deviceOpReal, deviceOpC, and 98 more.
Lemma 774 (rvdRC_apply). source ↗
Proof. Immediate from the definitions.
Used by rvdRC_isPositive, modConj_projIK_modConj, modConj_projK_modConj.
Lemma 775 (rvdRC_isSymmetric). source ↗
Rℂ is complex-symmetric: ⟪Rℂ x, y⟫_ℂ = ⟪x, Rℂ y⟫_ℂ. Re is rvdR_inner_symm; Im follows from it via the i-twist and ℂ-linearity (rvdR_smul_I).
Proof. By rvdR, rvdR_inner_symm, rvdR_smul_I.
Used by rvdRC_isPositive, rvdTwoSubRC_isSymmetric, diagInt_specCoord.
Lemma 776 (rvdRC_isPositive). source ↗
Rℂ is a positive operator in the complex C*-algebra H →L[ℂ] H. Self-adjoint (rvdRC_isSymmetric) with 0 ≤ Re⟪Rℂ x, x⟫ = ⟪R x, x⟫_ℝ (rvdR_inner_self_nonneg). Hence 0 ≤ Rℂ in the Loewner order and the continuous functional calculus square root CFC.sqrt (Rℂ) — the R^{1/2} factor of the Rieffel–Van Daele polar decomposition — is available.
Proof. By rvdR, rvdR_inner_self_nonneg, rvdRC_apply, rvdRC_isSymmetric.
Used by rvdRC_nonneg.
Lemma 777 (rvdRC_nonneg). source ↗
0 ≤ Rℂ in the Loewner order (operator nonnegativity), from rvdRC_isPositive.
This is the maximal honest step toward the RvD square root R^{1/2} right now: Rℂ is a genuine positive operator, so R^{1/2} = CFC.sqrt Rℂ is mathematically available — but the Mathlib CFC.sqrt requires StarOrderedRing (H →L[ℂ] H), an instance Mathlib has NOT yet established for operator algebras (it is flagged as future work in InnerProductSpace/Positive.lean: “when we have StarOrderedRing (E →L[𝕜] E)”). So the polar-decomposition factor R^{1/2} is blocked on that single missing instance, not on our construction; rvdRC_isPositive/rvdRC_nonneg is exactly the hypothesis the square root will consume once it lands.
Proof. By rvdRC_isPositive.
Used by rvdSqrtR_mul_self, rvdRC_isSelfAdjoint, rvdRC_spectrum_mem_Icc, rvdPmQ_commute_rvdT.
Definition 778 (rvdPmQ). source ↗
RvD P − Q — the self-adjoint operator whose polar decomposition JT = P − Q (RvD Definition 2.1) yields the modular conjugation J and the positive T.
Used by rvdPmQ_isSelfAdjoint, rvdPmQ_eq_zero, rvdPmQ_injective, rvdPmQ_smul_I, rvdRC_mul_rvdTwoSubRC_apply, rvdPmQ_commute_A, rvdT_injective, rvdT_norm_eq, and 31 more.
Lemma 779 (rvdPmQ_isSelfAdjoint). source ↗
P − Q is self-adjoint (its polar decomposition J·T then has J self-adjoint, T ≥ 0).
Proof. By projK, projIK, projK_isSelfAdjoint, projIK_isSelfAdjoint.
Used by rvdT_norm_eq, rvdPmQ_commute_rvdT.
Lemma 780 (rvdPmQ_eq_zero). source ↗
D = P − Q is injective (kernel-free). Dξ = 0 ⟹ Pξ = Qξ ∈ 𝒦 ∩ i𝒦 = {0} (IsSeparating), so Pξ = Qξ = 0, whence Rξ = Pξ + Qξ = 0 and ξ = 0 (rvdR_eq_zero). Injectivity of D is what makes the modular conjugation J (of D = J·T) a full involution J² = 1 rather than a partial isometry.
Proof. By projK, projIK, rvdR, rvdR_apply, rvdR_eq_zero.
Used by rvdPmQ_injective.
Lemma 781 (rvdPmQ_injective). source ↗
D = P − Q is injective.
Proof. By rvdPmQ_eq_zero.
Used by rvdT_injective, rvdRC_mul_rvdTwoSubRC_injective.
Lemma 782 (rvdR_le_two). source ↗
RvD upper bound R ≤ 2 (operator form): 2·1 − R is positive. With rvdR_isPositive (0 ≤ R) this is the complete RvD bound 0 ≤ R ≤ 2 at the operator level — 2 − R is then also positive, so BOTH R^{1/2} and (2 − R)^{1/2} exist by the continuous functional calculus, the two factors of the polar decomposition T = R^{1/2}(2 − R)^{1/2} (RvD Prop 2.2(2)).
Proof. By projK, projIK, rvdR_inner_self_le, rvdR_inner_symm.
Used by rvdTwoSubRC_isPositive.
Lemma 783 (rvdPmQ_smul_I). source ↗
D = P − Q is conjugate-linear (anti-ℂ-linear): D(i·ξ) = −i·(D ξ). In contrast to the ℂ-linear R = P + Q (rvdR_smul_I), the difference D anticommutes with mult-by-i — this is exactly the structural reason the modular conjugation J of the polar decomposition J·T = P − Q is antiunitary (conjugate-linear) rather than unitary. Immediate from the conjugation identities projK_smul_I, projIK_smul_I.
Proof. By projK, projIK, projIK_smul_I, projK_smul_I.
Used by rvdPmQ_smul_conj.
Definition 784 (rvdTwoSubRC). source ↗
RvD 2 − R as a ℂ-linear operator. With 0 ≤ R (rvdRC_nonneg) and R ≤ 2 this is the second positive factor (2 − R) whose square root pairs with R^{1/2} in T = R^{1/2}(2 − R)^{1/2}.
Used by cfcCont_sqrtTwoSub_eq, rvdTwoSubRC_apply, rvdTwoSubRC_isSymmetric, rvdTwoSubRC_isPositive, rvdTwoSubRC_nonneg, rvdSqrtTwoSubR, rvdSqrtTwoSubR_nonneg, rvdSqrtTwoSubR_mul_self, and 33 more.
Lemma 785 (rvdTwoSubRC_apply). source ↗
Used by rvdTwoSubRC_isSymmetric, rvdRC_mul_rvdTwoSubRC_apply, rvdPmQ_commute_rvdT, modConj_projIK_modConj, modConj_projK_modConj, rvdPmQ_mul_rvdRC_rs, rvdRC_E_two_levelSet, modUnitary_commute_rvdPmQ_rs.
Lemma 786 (rvdTwoSubRC_isSymmetric). source ↗
2 − R is complex-symmetric (1 and Rℂ both are).
Proof. By rvdR, rvdRC, rvdRC_isSymmetric, rvdTwoSubRC_apply.
Used by rvdTwoSubRC_isPositive.
Lemma 787 (rvdTwoSubRC_isPositive). source ↗
0 ≤ 2 − R (the upper RvD bound R ≤ 2 in operator form). The pointwise reApplyInnerSelf of the ℂ-operator (2:ℂ)•1 − Rℂ is definitionally that of the ℝ-operator (2:ℝ)•1 − R (both are Re⟪(2 • x − R x), x⟫, and (2:ℂ)•x = (2:ℝ)•x), so positivity transfers directly from the already-proven rvdR_le_two.
Proof. By rvdR, rvdR_le_two, rvdTwoSubRC_isSymmetric.
Used by rvdTwoSubRC_nonneg, rvdRC_spectrum_mem_Icc.
Lemma 788 (rvdTwoSubRC_nonneg). source ↗
0 ≤ 2 − R in the Loewner order.
Proof. By rvdTwoSubRC_isPositive.
Used by rvdSqrtTwoSubR_mul_self, rvdRC_spectrum_mem_Icc, rvdPmQ_commute_rvdT.
Definition 789 (rvdSqrtR). source ↗
RvD R^{1/2} — the continuous-functional-calculus square root of R, now available.
Used by h1_of_stripKMSrvd, gConstancy_of_inputs, oneParticleBW_of_inputs, oneParticleBW_of_stripKMSrvd_density, gConstancy_entire, gFunction_top_edge_real_all, gConstancy_entire_of_bottom, gConstancy_eta_of_bottom, and 32 more.
Definition 790 (rvdSqrtTwoSubR). source ↗
RvD (2 − R)^{1/2}.
Used by deviceOpC_neg_half_eq, modConj_deviceOpC_neg_half, cfcCont_sqrtTwoSub_eq, rvdSqrtTwoSubR_nonneg, rvdSqrtTwoSubR_mul_self, rvdSqrtR_commute_rvdSqrtTwoSubR, rvdT, rvdT_sq, and 12 more.
Lemma 791 (rvdSqrtR_nonneg). source ↗
0 ≤ R^{1/2}.
Proof. By rvdRC.
Used by rvdT_nonneg, modConj_rvdSqrtR_modConj.
Lemma 792 (rvdSqrtTwoSubR_nonneg). source ↗
0 ≤ (2 − R)^{1/2}.
Proof. By rvdTwoSubRC.
Used by rvdT_nonneg.
Lemma 793 (rvdSqrtR_mul_self). source ↗
R^{1/2} · R^{1/2} = R.
Proof. By rvdRC_nonneg.
Used by rvdT_sq, modConjSqrtR_sq.
Lemma 794 (rvdSqrtTwoSubR_mul_self). source ↗
(2 − R)^{1/2} · (2 − R)^{1/2} = 2 − R.
Proof. By rvdTwoSubRC_nonneg.
Used by rvdT_sq, rvdSqrtTwoSubR_injective, rvdSqrtR_modConj_of_mem_K.
Lemma 795 (rvdRC_commute_rvdTwoSubRC). source ↗
R and 2 − R commute (the second is 2·1 − R, an affine function of the first).
Proof. Immediate from the definitions.
Used by rvdSqrtR_commute_rvdSqrtTwoSubR, rvdPmQ_commute_rvdT, rvdRC_commute_rvdT, rvdRC_mul_rvdTwoSubRC_isSelfAdjoint, rvdRC_injective.
Lemma 796 (rvdSqrtR_commute_rvdSqrtTwoSubR). source ↗
The square roots commute: √R = cfcₙ √ R commutes with 2 − R (a function of R), and then with √(2 − R) = cfcₙ √ (2 − R). Both applications use Commute.cfcₙ_nnreal (CFC.sqrt = cfcₙ NNReal.sqrt).
Proof. By rvdRC, rvdTwoSubRC, rvdRC_commute_rvdTwoSubRC.
Used by rvdT_sq, rvdT_nonneg, modConj_rvdT_modConj, modConj_fixed_of_sqrtR_mem_K.
Definition 797 (rvdT). source ↗
RvD T — the positive part of the polar decomposition J·T = P − Q, T = R^{1/2}(2 − R)^{1/2}.
Used by rvdT_sq, rvdT_nonneg, rvdT_isSelfAdjoint, rvdT_injective, rvdT_norm_eq, rvdPmQ_commute_rvdT, rvdPmQ_commute_rvdT_apply, rvdT_restrictScalars_denseRange, and 18 more.
Lemma 798 (rvdT_sq). source ↗
RvD Prop 2.2(2): T² = R(2 − R). Using that R^{1/2} and (2 − R)^{1/2} commute, the product T² = R^{1/2}(2−R)^{1/2}R^{1/2}(2−R)^{1/2} regroups into (R^{1/2})²((2−R)^{1/2})² = R(2−R). With J² = 1 and JT = P − Q, this is (P − Q)² = R(2 − R) — the modular-operator factorization.
Proof. By rvdSqrtR, rvdSqrtTwoSubR, rvdSqrtR_mul_self, rvdSqrtTwoSubR_mul_self, rvdSqrtR_commute_rvdSqrtTwoSubR.
Used by rvdT_injective, rvdT_norm_eq, rvdPmQ_commute_rvdT.
Lemma 799 (rvdT_nonneg). source ↗
T = R^{1/2}(2−R)^{1/2} is positive — a product of two commuting positive operators.
Proof. By rvdSqrtR, rvdSqrtTwoSubR, rvdSqrtR_nonneg, rvdSqrtTwoSubR_nonneg, rvdSqrtR_commute_rvdSqrtTwoSubR.
Used by rvdT_isSelfAdjoint, rvdPmQ_commute_rvdT.
Lemma 800 (rvdT_isSelfAdjoint). source ↗
T is self-adjoint (it is positive).
Proof. By rvdT_nonneg.
Used by rvdT_norm_eq, rvdT_restrictScalars_denseRange, rvdT_real_inner_symm.
Lemma 801 (rvdRC_mul_rvdTwoSubRC_apply). source ↗
T² = D² as maps: (R(2−R)) ξ = (P − Q)((P − Q) ξ). Both sides reduce to P ξ + Q ξ − P(Q ξ) − Q(P ξ) by idempotency of P, Q (R² = R + (PQ+QP), so R(2−R) = 2R − R² = R − (PQ+QP) = (P−Q)²). This is what transfers ‖T ξ‖ = ‖D ξ‖ (the modular conjugation is an isometry from T to D).
Proof. By projK, projIK, rvdR, projK_idem, projIK_idem, rvdTwoSubRC_apply.
Used by rvdPmQ_commute_A, rvdT_injective, rvdT_norm_eq, rvdRC_mul_rvdTwoSubRC_injective.
Lemma 802 (rvdPmQ_commute_A). source ↗
D commutes with A = R(2−R) = T² (the inductive base for D·T = T·D). Trivial because A = D² as maps (rvdRC_mul_rvdTwoSubRC_apply): D·D² = D³ = D²·D. The full D·√A = √A·D (the antilinear modular-conjugation commutation, whence J² = 1) follows from this base by the closed-commutant argument — {Y | D∘Y = Y∘D} is a closed real *-subalgebra ⊇ elemental ℝ A ∋ √A.
Proof. By rvdRC_mul_rvdTwoSubRC_apply.
Used by rvdPmQ_commute_rvdT, modUnitary_commute_rvdPmQ_rs.
Lemma 803 (rvdT_injective). source ↗
T = R^{1/2}(2−R)^{1/2} is injective. T² = R(2−R) = D² (rvdT_sq, rvdRC_mul_rvdTwoSubRC_apply) is injective because D = P−Q is (rvdPmQ_injective), and T injective follows. T injective ⟹ range T dense ((range T)‾ = (ker T)ᗮ = H), which is what makes the modular conjugation J : T ξ ↦ D ξ extend to all of H.
Proof. By rvdRC, rvdPmQ, rvdPmQ_injective, rvdTwoSubRC, rvdT_sq, rvdRC_mul_rvdTwoSubRC_apply.
Used by rvdT_restrictScalars_denseRange, modConj_fixed_of_sqrtR_mem_K.
Lemma 804 (rvdT_norm_eq). source ↗
The modular-conjugation isometry: ‖T ξ‖ = ‖D ξ‖ (RvD polar decomposition D = J·T). D = P − Q is conjugate-linear and T = R^{1/2}(2−R)^{1/2} is its positive modulus |D|; the map J : T ξ ↦ D ξ is therefore a well-defined antiunitary (the modular conjugation). Proved from T² = D² (rvdRC_mul_rvdTwoSubRC_apply via rvdT_sq) and self-adjointness of both T and D.
Proof. By rvdRC, rvdPmQ_isSelfAdjoint, rvdTwoSubRC, rvdT_sq, rvdT_isSelfAdjoint, rvdRC_mul_rvdTwoSubRC_apply.
Used by modConj_rvdT, modConj_norm.
Lemma 805 (rvdPmQ_mul_rvdR). source ↗
RvD intertwiner D·R = (2−R)·D.
Proof. By projK, projIK, projK_idem, projIK_idem.
Used by rvdPmQ_anticommute_rvdR_sub_one, rvdPmQ_mul_rvdRC_rs.
Lemma 806 (rvdPmQ_anticommute_rvdR_sub_one). source ↗
D ANTICOMMUTES with R − 1: D·(R−1) = −(R−1)·D. Because D·R = (2−R)·D (rvdPmQ_mul_rvdR), so D·(R−1) = (2−R)·D − D = (1−R)·D = −(R−1)·D. This is the engine for the modular covariance [U_t, D] = 0: D antilinear + D·(R−1)=−(R−1)·D makes D COMMUTE with i·(R−1), and U_t = u_t(R) is (a Borel function) of i·(R−1) with conj(u_t(2−r)) = u_t(r).
Proof. By rvdPmQ_mul_rvdR.
Used by rvdPmQ_rvdRC.
Lemma 807 (rvdPmQ_smul_conj). source ↗
D is conjugate-(ℂ-)linear: D(c•ξ) = conj(c)·Dξ for every c : ℂ. From ℝ-linearity plus the i-case rvdPmQ_smul_I (D(i•ξ)=−i•Dξ), expanding c = c.re + c.im·i.
Proof. By rvdPmQ_smul_I.
Used by cfcΩ_intertwine.
← all sections · ← SpectralTheorem · StandardSubspaceModularFlow →