feat(QuantumInfo): discharge sorries in ClassicalInfo.Capacity and Regularized

QuantumInfo/Finite/Capacity.lean

@@ -25,7 +25,8 @@ The most basic facts:
  * `emulates_self`: Every channel emulates itself.
  * `emulates_trans`: If A emulates B and B emulates C, then A emulates C. (That is, emulation is an ordering.)
  * `εApproximates A B ε` is equivalent to the existence of some δ (depending ε and dims(A)) so that |A-B| has diamond norm at most δ, and δ→0 as ε→0.
- * `achievesRate_0`: Every channel achievesRate 0. So, the set of achievable rates is Nonempty.
+ * `achievesRate_0`: Every channel between nonempty spaces achievesRate 0. So, in that case,
+   the set of achievable rates is Nonempty.
  * If a channel achievesRate R₁, it also every achievesRate R₂ every R₂ ≤ R₁, i.e. it is an interval extending left towards -∞. Achievable rates are `¬BddBelow`.
  * `bddAbove_achievesRate`: A channel C : dimX → dimY cannot achievesRate R with `R > log2(min(dimX, dimY))`. Thus, the interval is `BddAbove`.
 
@@ -122,19 +123,19 @@ end εApproximates
 
 section AchievesRate
 
-/-- Every quantum channel achieves a rate of zero. -/
-theorem achievesRate_0 (Λ : CPTPMap d₁ d₂) : Λ.AchievesRate 0 := by
+/-- Every quantum channel between nonempty spaces achieves a rate of zero. -/
+theorem achievesRate_0 (Λ : CPTPMap d₁ d₂) [Nonempty d₁] [Nonempty d₂] : Λ.AchievesRate 0 := by
   intro ε hε
   use 1, zero_lt_one, 1, default
   constructor
-  · have : Nonempty d₁ := by sorry--having a CPTPMap should be enough to conclude in- and out-spaces are nonempty
-    have : Nonempty d₂ := by sorry
-    use Classical.ofNonempty, Classical.ofNonempty
-    sorry--exact Unique.eq_default _
+  · refine ⟨(default : CPTPMap (Fin 1) (Fin 1 → d₁)),
+      (default : CPTPMap (Fin 1 → d₂) (Fin 1)), ?_⟩
+    exact CPTPMap.eq_if_output_unique _ _
   constructor
   · norm_num
-  · rw [Unique.eq_default id]
-    sorry--apply εApproximates_monotone (εApproximates_self default) hε.le
+  · have hB : (default : CPTPMap (Fin 1) (Fin 1)) = CPTPMap.id := CPTPMap.eq_if_output_unique _ _
+    simpa [hB] using
+      εApproximates_monotone (εApproximates_self (CPTPMap.id (dIn := Fin 1))) hε.le
 
 /-- The identity channel on D dimensional space achieves a rate of log2(D). -/
 theorem id_achievesRate_log_dim : (id (dIn := d₁)).AchievesRate (Real.logb 2 (Fintype.card d₁)) := by
@@ -199,8 +200,9 @@ end AchievesRate
 
 section capacity
 
-/-- Quantum channel capacity is nonnegative. -/
-theorem zero_le_quantumCapacity (Λ : CPTPMap d₁ d₂) : 0 ≤ Λ.quantumCapacity :=
+/-- Quantum channel capacity is nonnegative for channels between nonempty spaces. -/
+theorem zero_le_quantumCapacity (Λ : CPTPMap d₁ d₂) [Nonempty d₁] [Nonempty d₂] :
+    0 ≤ Λ.quantumCapacity :=
   le_csSup (bddAbove_achievesRate Λ) (achievesRate_0 Λ)
 
 /-- Quantum channel capacity is at most log2(D), where D is the input dimension. -/

QuantumInfo/Regularized.lean

@@ -7,6 +7,7 @@ module
 
 public import QuantumInfo.ForMathlib.Superadditive
 public import Mathlib.Order.LiminfLimsup
+public import Mathlib.Topology.Order.LiminfLimsup
 public import Mathlib.Topology.Order.MonotoneConvergence
 
 /-! Definition of "Regularized quantities" as are common in information theory,
@@ -120,27 +121,43 @@ end SupRegularized
 
 section real
 
+private def realNegOrderIso : ℝ ≃o ℝᵒᵈ where
+  toEquiv := Equiv.neg ℝ
+  map_rel_iff' := by
+    intro a b
+    change (-b : ℝ) ≤ -a ↔ a ≤ b
+    simpa using neg_le_neg_iff
+
+private theorem limsup_eq_neg_liminf_neg {fn : ℕ → ℝ} {_lb _ub : ℝ}
+    (hl : ∀ n, _lb ≤ fn n) (hu : ∀ n, fn n ≤ _ub) :
+    Filter.atTop.limsup fn = -Filter.atTop.liminf (fun n => -fn n) := by
+  have hneg : -Filter.atTop.limsup fn = Filter.atTop.liminf (fun n => -fn n) := by
+    have hdual := OrderIso.limsup_apply (f := Filter.atTop) (u := fn) realNegOrderIso
+      (hu := Filter.isBoundedUnder_of_eventually_le (f := Filter.atTop) (u := fn)
+        (Filter.Eventually.of_forall hu))
+      (hu_co := Filter.isCoboundedUnder_le_of_le Filter.atTop hl)
+      (hgu := Filter.isBoundedUnder_of_eventually_le (α := ℝᵒᵈ) (f := Filter.atTop)
+        (u := fun n => (-fn n : ℝᵒᵈ)) (Filter.Eventually.of_forall fun n => neg_le_neg (hu n)))
+      (hgu_co := Filter.isCoboundedUnder_le_of_le (α := ℝᵒᵈ) Filter.atTop
+        (f := fun n => (-fn n : ℝᵒᵈ)) (x := (-_lb : ℝᵒᵈ)) fun n => neg_le_neg (hl n))
+    simpa [Filter.limsup, Filter.liminf, Filter.limsSup, Filter.limsInf, realNegOrderIso] using
+      congrArg OrderDual.ofDual hdual
+  linarith
+
 variable {fn : ℕ → ℝ} {_lb _ub : ℝ} {hl : ∀ n, _lb ≤ fn n} {hu : ∀ n, fn n ≤ _ub}
 
 theorem InfRegularized.to_SupRegularized : InfRegularized fn hl hu = -SupRegularized (-fn ·)
     (lb := -_ub) (ub := -_lb) (neg_le_neg_iff.mpr <| hu ·) (neg_le_neg_iff.mpr <| hl ·) := by
-  sorry
+  unfold InfRegularized SupRegularized
+  have h : -Filter.atTop.liminf fn = Filter.atTop.limsup (fun n => -fn n) := by
+    simpa using (limsup_eq_neg_liminf_neg (fn := fun n => -fn n)
+      (hl := fun n => neg_le_neg (hu n)) (hu := fun n => neg_le_neg (hl n))).symm
+  linarith
 
 theorem SupRegularized.to_InfRegularized : SupRegularized fn hl hu = -InfRegularized (-fn ·)
     (lb := -_ub) (ub := -_lb) (neg_le_neg_iff.mpr <| hu ·) (neg_le_neg_iff.mpr <| hl ·) := by
-  -- By definition of `InfRegularized` and `SupRegularized`, we can rewrite the goal using the fact that the liminf of a function is the negative of the limsup of its negative.
-  have h_limsup_limsup : Filter.limsup fn Filter.atTop = -Filter.liminf (fun n => -fn n) Filter.atTop := by
-    -- By definition of liminf and limsup, we know that for any sequence of real numbers, the liminf of the negative of the sequence is the negative of the limsup of the original sequence.
-    have h_limsup_neg : ∀ (s : ℕ → ℝ), Filter.liminf (fun n => -s n) Filter.atTop = -Filter.limsup s Filter.atTop := by
-      -- Apply the definition of liminf and limsup.
-      intros s
-      rw [Filter.liminf_eq, Filter.limsup_eq];
-      -- By definition of supremum and infimum, we know that the supremum of a set is the negative of the infimum of its negative.
-      have h_sup_neg_inf : ∀ (S : Set ℝ), sSup S = -sInf (-S) := by
-        intro S; rw [ Real.sInf_def ] ; aesop;
-      convert h_sup_neg_inf _ using 3 ; aesop;
-    rw [ h_limsup_neg, neg_neg ];
-  exact h_limsup_limsup
+  unfold InfRegularized SupRegularized
+  exact limsup_eq_neg_liminf_neg hl hu
 
 /-- For `Antitone` functions, the value `Filter.Tendsto` the `InfRegularized` value. -/
 theorem InfRegularized.anti_tendsto (h : Antitone fn) :
@@ -163,6 +180,12 @@ theorem InfRegularized.of_Subadditive (hf : Subadditive (fun n ↦ fn n * n))
       convert Or.inr (hl (n+1))
       field_simp
   )
-  apply tendsto_nhds_unique h₁
-  have := InfRegularized.anti_tendsto (fn := fn) (hl := hl) (hu := hu) (sorry)
-  sorry
+  have heq : (fun n => fn n * n / n) =ᶠ[Filter.atTop] fn := by
+    refine (Filter.eventually_atTop.2 ?_ : (fun n => fn n * n / n) =ᶠ[Filter.atTop] fn)
+    refine ⟨1, ?_⟩
+    intro n hn
+    have hn' : (n : ℝ) ≠ 0 := by
+      exact_mod_cast Nat.ne_of_gt (Nat.succ_le_iff.mp hn)
+    field_simp [hn']
+  have hfn : Filter.Tendsto fn .atTop (nhds hf.lim) := (Filter.tendsto_congr' heq).1 h₁
+  exact (Filter.Tendsto.liminf_eq hfn).symm