Project-declaredLean 4.28.0 · mathlib@8f9d9cff6bd7

Sᵥₙ wm

Sᵥₙ_wm

quantum information entropy quantum channels ssa

Plain-language statement

Weak monotonicity, version with partial traces.

Exact Lean statement

lemma Sᵥₙ_wm (ρ : MState (d₁ × d₂ × d₃)) :
    Sᵥₙ ρ.traceRight + Sᵥₙ ρ.traceLeft.traceLeft ≤
    Sᵥₙ ρ.assoc'.traceRight + Sᵥₙ ρ.traceLeft

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

lemma Sᵥₙ_wm (ρ : MState (d₁ × d₂ × d₃)) :    Sᵥₙ ρ.traceRight + Sᵥₙ ρ.traceLeft.traceLeft ≤    Sᵥₙ ρ.assoc'.traceRight + Sᵥₙ ρ.traceLeft := by  have h_ne123 := ρ.nonempty  obtain ⟨ ρn, hρn_pos, hρn ⟩ := MState.approx_by_pd ρ;  -- Apply the inequality for each ρn and then take the limit.  have h_lim : Filter.Tendsto (fun n => Sᵥₙ (ρn n).traceRight + Sᵥₙ (ρn n).traceLeft.traceLeft) Filter.atTop (nhds (Sᵥₙ ρ.traceRight + Sᵥₙ ρ.traceLeft.traceLeft)) ∧ Filter.Tendsto (fun n => Sᵥₙ (ρn n).assoc'.traceRight + Sᵥₙ (ρn n).traceLeft) Filter.atTop (nhds (Sᵥₙ ρ.assoc'.traceRight + Sᵥₙ ρ.traceLeft)) := by    constructor <;> refine' Filter.Tendsto.add _ _;    · exact Sᵥₙ_continuous.continuousAt.tendsto.comp ( MState.traceRight_continuous.continuousAt.tendsto.comp hρn );    · exact Sᵥₙ_continuous.comp ( MState.traceLeft_continuous.comp ( MState.traceLeft_continuous ) ) |> fun h => h.continuousAt.tendsto.comp hρn;    · convert Sᵥₙ_continuous.continuousAt.tendsto.comp ( MState.traceRight_continuous.continuousAt.tendsto.comp ( MState.assoc'_continuous.continuousAt.tendsto.comp hρn ) ) using 1;    · exact Sᵥₙ_continuous.continuousAt.tendsto.comp ( MState.traceLeft_continuous.continuousAt.tendsto.comp hρn );  have ⟨_, hn23⟩ := nonempty_prod.mp h_ne123  have ⟨_, _⟩ := nonempty_prod.mp hn23  exact le_of_tendsto_of_tendsto' h_lim.1 h_lim.2 fun n => Sᵥₙ_wm_pd _ ( hρn_pos n )

Project: quantumInfo
License: MIT
Commit: 56e83a9288a3
Source: QuantumInfo/Finite/Entropy/SSA.lean:1048-1062

Reuse this declaration

Bring the exact result into your workflow

The import identifies the source module. Your project still needs the pinned package dependency shown on this page.

What this badge means

This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.

Continue in this project

Related declarations

Project-declaredLean 4.28.0

Conj Transpose isometry mul isometry le one

conjTranspose_isometry_mul_isometry_le_one

Project documentation

The operator norm of the conjugate transpose is equal to the operator norm. -/ theorem Matrix.opNorm_conjTranspose_eq_opNorm {m n : Type*} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (A : Matrix m n 𝕜) : Matrix.opNorm Aᴴ = Matrix.opNorm A := by unfold Matrix.opNorm rw [← ContinuousLinearMap.adjoint.norm_map (toEuclideanLin A).toContinuousLine...

quantum informationentropyquantum channels

Source project: quantumInfo

Person-level attribution pending.

View proof record

Project-declaredLean 4.28.0

Convex roof of pure

convex_roof_of_pure

Plain-language statement

The convex roof extension of g : KetUpToPhase d → ℝ≥0 applied to a pure state ψ is g (KetUpToPhase.mk ψ).

quantum informationentropyquantum channels

Source project: quantumInfo

Person-level attribution pending.

View proof record

Project-declaredLean 4.28.0

Id achieves Rate log dim

CPTPMap.id_achievesRate_log_dim

Plain-language statement

The identity channel on D dimensional space achieves a rate of log2(D).

quantum informationentropyquantum channels

Source project: quantumInfo

Person-level attribution pending.

View proof record