Coarse-graining a preparation does not decrease its entropy

Category: 3-Local (W8 applied; the coarse-graining half of W4 in specs/qit-chain-scoping.md).

A preparation on Σ that is a mixture of preparations, μ = ∑ᵢ cᵢ μᵢ, has for its density operator the mixture of the components' density operators, because the barycentre is affine in the measure (barycenterMatrix_finset_sum_smul). Concavity of the von Neumann entropy (Mathlib/QuantumInfo/ConcavityFull.lean) then says:

• ★★ vonNeumannEntropy_barycenter_mixture_ge, ★★ preparationEntropy_mixture_ge — the entropy of the mixed preparation is at least the weighted average of the entropies of the components. Forgetting which component prepared the system (coarse-graining the preparation) costs entropy on average, never gains it.

Supporting: isProbabilityMeasure_finset_sum_smul (a mixture of probability measures with weights summing to one is one), map_finset_sum_smul (pushforward is affine).

Honest scope

No support hypothesis (since ConcavityFull.lean). The components are arbitrary preparations on Σ; "coarse-graining of regions" is the case where the μᵢ are the conditional measures of a partition of a region and the cᵢ their Liouville weights, which is one instance of this statement.

References: specs/qit-chain-scoping.md (W4, W8); LF2/PreparationQdensity.lean (W2); LF2/PreparationBarycenter.lean (W3); Mathlib/QuantumInfo/ConcavityFull.lean.

Coarse-graining a preparation does not decrease its entropy

theorem CSD.LF2.barycenterMatrix_finset_sum_smul {ι : Type u_1} [Fintype ι] {Q : Type u_2} [MeasurableSpace Q] {N : ℕ} (rep : Q → EuclideanSpace ℂ (Fin N)) (hrep_unit : ∀ (p : Q), ‖rep p‖ = 1) (hrep_meas : Measurable rep) (c : ι → ℝ) (hc : ∀ (i : ι), 0 ≤ c i) (μ : ι → MeasureTheory.Measure Q) [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)] : barycenterMatrix rep (∑ i : ι, ENNReal.ofReal (c i) • μ i) = ∑ i : ι, ↑(c i) • barycenterMatrix rep (μ i)

The barycentre is affine in the measure: along a finite mixture ∑ᵢ cᵢ • μᵢ of finite measures it is the mixture of the barycentres.

theorem CSD.LF2.isProbabilityMeasure_finset_sum_smul {ι : Type u_1} [Fintype ι] {Q : Type u_2} [MeasurableSpace Q] (c : ι → ℝ) (hc : ∀ (i : ι), 0 ≤ c i) (hc1 : ∑ i : ι, c i = 1) (μ : ι → MeasureTheory.Measure Q) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] : MeasureTheory.IsProbabilityMeasure (∑ i : ι, ENNReal.ofReal (c i) • μ i)

A finite mixture of probability measures with non-negative weights summing to one is a probability measure.

theorem CSD.LF2.vonNeumannEntropy_barycenter_mixture_ge {ι : Type u_1} [Fintype ι] {Q : Type u_2} [MeasurableSpace Q] {N : ℕ} (rep : Q → EuclideanSpace ℂ (Fin N)) (hrep_unit : ∀ (p : Q), ‖rep p‖ = 1) (hrep_meas : Measurable rep) (c : ι → ℝ) (hc : ∀ (i : ι), 0 ≤ c i) (hc1 : ∑ i : ι, c i = 1) (μ : ι → MeasureTheory.Measure Q) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] : ∑ i : ι, c i * QuantumInfo.vonNeumannEntropy ⋯ ≤ QuantumInfo.vonNeumannEntropy ⋯

★★ Coarse-graining does not decrease entropy, on average. For preparations μᵢ on the projective target with weights pᵢ, the entropy of the barycentre of the mixture is at least the weighted average of the entropies of the barycentres of the components. Forgetting which component prepared the system costs entropy. No support hypothesis.

theorem CSD.LF2.map_finset_sum_smul {ι : Type u_1} [Fintype ι] {α : Type u_3} {β : Type u_4} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) (hf : Measurable f) (c : ι → ENNReal) (μ : ι → MeasureTheory.Measure α) : MeasureTheory.Measure.map f (∑ i : ι, c i • μ i) = ∑ i : ι, c i • MeasureTheory.Measure.map f (μ i)

Pushing a finite mixture of measures forward is the mixture of the pushforwards.

theorem CSD.LF2.preparationEntropy_mixture_ge {ι : Type u_1} [Fintype ι] {N : ℕ} {SigmaSpace : Type u_3} {P : Type u_4} {G : Type u_5} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] (D : SectorData SigmaSpace P G) (μFS : MeasureTheory.Measure P) [MeasureTheory.IsProbabilityMeasure μFS] (bridge : MeasureBridgeData D μFS) (c : ι → ℝ) (hc : ∀ (i : ι), 0 ≤ c i) (hc1 : ∑ i : ι, c i = 1) (μprep : ι → MeasureTheory.Measure SigmaSpace) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μprep i)] (rep : P → EuclideanSpace ℂ (Fin N)) (hrep_unit : ∀ (p : P), ‖rep p‖ = 1) (hrep_meas : Measurable rep) : ∑ i : ι, c i * preparationEntropy D μFS bridge (μprep i) rep hrep_unit hrep_meas ≤ preparationEntropy D μFS bridge (∑ i : ι, ENNReal.ofReal (c i) • μprep i) rep hrep_unit hrep_meas

★★ Coarse-graining a preparation on Σ does not decrease its entropy, on average (W4's second half). For preparations μᵢ on Σ mixed with weights cᵢ, the entropy of the mixed preparation is at least the weighted average of the entropies of the components. No support hypothesis.