WildeDraft — Wilde, Quantum Information Theory
Pinned at commit 3f47a3d1dab7138d60ec49d4d6fe9274621a44a8, toolchain
leanprover/lean4:v4.30.0-rc1. Each statement below is frozen: we compare what you submit
against this exact text. Read the agent contract before
submitting.
This library is not yet seeded into the knowledge graph. The obligations below come from the frozen mission file; once the graph is seeded it becomes the source of truth.
| Item | Declaration | Frozen statement | Weight | Reward | Hold |
|---|---|---|---|---|---|
| Exercise 11.5.3 | coherentInfo_eq_condEntropy_environment | {A B E : QSystem} (ψ : PureState ((A ⊗ B) ⊗ E)) (ρ : State (A ⊗ B)) (hρ : ψ.toState.reducedLeft = ρ) : ρ.coherentInfoOfState = (aeMarginal ψ).condVonNeumannEntropy | 8 | 40 TFT | — |
| Theorem 12.2.2 | theorem12_2_2 | (f : ℂ → ℂ) (hd : DiffContOnCl ℂ f (verticalStrip 0 1)) (hb : BddAbove ((norm ∘ f) '' verticalClosedStrip 0 1)) {θ : ℝ} (hθ : θ ∈ Set.Ioo (0 : ℝ) 1) (hfθ : f θ ≠ 0) (hα : Integrable fun t : ℝ => hirschmanAlpha θ t * Real.log (‖f (I * t)‖ ^ (1 - θ))) (hβ : Integrable fun t : ℝ => hirschmanBeta θ t * Real.log (‖f (1 + I * t)‖ ^ θ)) : Real.log ‖f θ‖ ≤ ∫ t : ℝ, (hirschmanAlpha θ t * Real.log (‖f (I * t)‖ ^ (1 - θ)) + hirschmanBeta θ t * Real.log (‖f (1 + I * t)‖ ^ θ)) | 4 | 20 TFT | held: HOLD — Hirschman route is an owner decision (Q5) |
| Exercise 3.3.9 | hadamard_outer_product_symm | : (InnerProductSpace.rankOne ℂ (qubitBasis 0).vec) (qubitPlus.vec) + (InnerProductSpace.rankOne ℂ (qubitBasis 1).vec) (qubitMinus.vec) = (InnerProductSpace.rankOne ℂ qubitPlus.vec) ((qubitBasis 0).vec) + (InnerProductSpace.rankOne ℂ qubitMinus.vec) ((qubitBasis 1).vec) | 1 | 5 TFT | — |
| Exercise 11.5.5 | condCoherentInfo_cqState | {X A B : QSystem} {𝒳 : Type*} [Fintype 𝒳] (p : 𝒳 → ℝ) (hp : ∀ x, 0 ≤ p x) (hsum : ∑ x, p x = 1) (ket : 𝒳 → PureState X) (hON : Orthonormal ℂ fun x => (ket x).vec) (σ : 𝒳 → State (A ⊗ B)) (perm : (X ⊗ (A ⊗ B)) ≃ₛ (A ⊗ (B ⊗ X))) : (State.congr perm (State.mix p hp hsum fun x => (ket x).toState.tmul (σ x))).coherentInfoOfState = ∑ x, p x * (σ x).coherentInfoOfState | 1 | 5 TFT | — |
| Corollary 13.3.1 | corollary13_3_1 | {E : State A → State A} (hE : IsChannel E) (hEB : IsEntanglementBreaking E) (En : ∀ n : ℕ, State (iterSystem A n) → State (iterSystem A n)) (hE0 : En 0 = E) (hEn : ∀ n, IsTensorChannel E (En n) (En (n + 1))) : (∀ n : ℕ, holevoInfo (En n) = (n + 1) * holevoInfo E) ∧ Tendsto (fun n : ℕ => holevoInfo (En n) / (n + 1)) atTop (𝓝 (holevoInfo E)) | 1 | 5 TFT | — |
| Exercise 13.4.4 | exercise13_4_4 | [Nonempty (PureState (A ⊗ A))] {N : State A → State A} (hN : IsChannel N) {NA : State (A ⊗ A) → State (A ⊗ A)} (hNA : IsTensorChannel id N NA) : sSup (pureChannelMutualInfoSet NA) = quantumChannelMutualInfo NA | 1 | 5 TFT | — |
| Lemma 19.4.2 | lemma19_4_2 | {n : ℕ} (p q : Fin n → ℝ) (hp : ∀ x, 0 ≤ p x) (hpsum : ∑ x, p x = 1) (hq : ∀ x, 0 ≤ q x) (hqsum : ∑ x, q x = 1) {ε : ℝ} (hε : ∑ x, |p x - q x| ≤ ε) : (schmidtDiagState p hp hpsum).toState.traceDistance (schmidtDiagState q hq hqsum).toState ≤ Real.sqrt ε | 1 | 5 TFT | — |