Channel

Difficulty: moderate — 4 definitions, 2 abbreviations, 0 lemmas, 3 theorems, 0 examples.

definition abbreviation theorem
legend
structure Channel (State Wire : Type) [Nonempty State] [Norm State] [Nonempty Wire] [Norm Wire] : Type
  • component : Component.Simplex State Wire Wire
  • rate : ℕ
Show details

Outer dependencies: (none)

Inner dependencies: Component.Simplex, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Eq, Fin, HEq, Nat, Nonempty, SizeOf, eq_of_heq

Used by: Channel.capacity, Channel.loss, Channel.lossless, Channel.lossless_stationary, Channel.lossy_loses_overall, Channel.overall_loss, Channel.system

abbrev Channel.system {State Wire : Type} [Nonempty State] [Norm State] [Nonempty Wire] [Norm Wire]
  (ch : Channel State Wire) : InformationSystem State Wire Wire
Show details 
| ch.system = ch.component.toInformationSystem

Complexity: 69 (size of the value term)

Outer dependencies: Channel, InformationSystem

Inner dependencies: Component.Simplex.toInformationSystem

Mathlib dependencies: Norm

Lean core dependencies: Nonempty

Used by: Channel.loss, Channel.lossless_stationary, Channel.lossy_loses_overall, Channel.overall_loss

def Channel.maxWireSize (Wire : Type) [Fintype Wire] [Nonempty Wire] [Norm Wire] : ℝ
Show details 
| Channel.maxWireSize Wire = Finset.univ.sup' ⋯ fun w => ‖w‖

Complexity: 45 (size of the value term)

Outer dependencies: (none)

Mathlib dependencies: Finset.sup', Finset.univ, Finset.univ_nonempty, Fintype, Norm, Real

Lean core dependencies: Nonempty

Used by: Channel.capacity

def Channel.capacity {State Wire : Type} [Nonempty State] [Norm State] [Nonempty Wire] [Norm Wire]
  [Fintype Wire] (ch : Channel State Wire) : ℝ
Show details 
| ch.capacity = ↑ch.rate * Channel.maxWireSize Wire

Complexity: 83 (size of the value term)

Outer dependencies: Channel

Inner dependencies: Channel.maxWireSize

Mathlib dependencies: Fintype, Norm, Real

Lean core dependencies: Nat.cast, Nonempty

Used by: (none)

abbrev Channel.loss {State Wire : Type} [Nonempty State] [Norm State] [Nonempty Wire] [Norm Wire]
  (ch : Channel State Wire) (s : State) (w : Wire) : ℝ
Show details 
| ch.loss s w = (ch.system.stepAt s w).delta

Complexity: 113 (size of the value term)

Outer dependencies: Channel

Inner dependencies: Channel.system, InformationSystem.Step.delta, InformationSystem.stepAt

Mathlib dependencies: Norm, Real

Lean core dependencies: Nonempty

Used by: Channel.lossless, Channel.lossless_stationary, Channel.lossy_loses_overall

def Channel.lossless {State Wire : Type} [Nonempty State] [Norm State] [Nonempty Wire] [Norm Wire]
  (ch : Channel State Wire) : Prop
Show details 
| ch.lossless = ∀ (s : State) (w : Wire), ch.loss s w = 0

Complexity: 73 (size of the value term)

Outer dependencies: Channel

Inner dependencies: Channel.loss

Mathlib dependencies: Norm, Real

Lean core dependencies: Eq, Nonempty

Used by: Channel.lossless_stationary

theorem Channel.overall_loss {State Wire : Type} [Nonempty State] [Norm State] [Nonempty Wire] [Norm Wire]
  (ch : Channel State Wire) (s : State) (ws : List Wire) :
  ‖(ch.system.eval s ws).1‖ - ‖s‖ = ws.totalSize - (ch.system.eval s ws).2.totalSize
Show details 
fun {State Wire} [Nonempty State] [Norm State] [Nonempty Wire] [Norm Wire] ch s ws =>
  InformationSystem.eval_delta ch.system s ws

Complexity: 79 (size of the value term)

Dependencies: Channel, Channel.system, InformationSystem.eval, List.totalSize

Proof dependencies: InformationSystem.eval_delta

Mathlib dependencies: Norm, Real

Lean core dependencies: Eq, List, Nonempty

Used by: (none)

theorem Channel.lossless_stationary {State Wire : Type} [Nonempty State] [Norm State] [Nonempty Wire]
  [Norm Wire] (ch : Channel State Wire) (hl : ch.lossless) (s : State) (w : Wire) :
  ‖(ch.system.step s w).1‖ = ‖s‖
Show details 
fun {State Wire} [Nonempty State] [Norm State] [Nonempty Wire] [Norm Wire] ch hl s w =>
  have h := hl s w;
  have this := InformationSystem.Step.delta_alt (ch.system.stepAt s w);
  Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt ‖(ch.system.step s w).1‖ ‖s‖
    (Not.intro fun a =>
      Mathlib.Tactic.Linarith.lt_irrefl
        (Eq.mp
          (congrArg (fun _a => _a < 0)
            (Mathlib.Tactic.Ring.of_eq
              (Mathlib.Tactic.Ring.Common.add_congr
                (Mathlib.Tactic.Ring.Common.add_congr
                  (Mathlib.Tactic.Ring.Common.neg_congr
                    (Mathlib.Tactic.Ring.Common.sub_congr
                      (Mathlib.Tactic.Ring.Common.sub_congr
                        (Mathlib.Tactic.Ring.Common.atom_pf ‖(ch.system.stepAt s w).input‖ rfl
                          (Eq.mpr
                            (id
                              (congrArg
                                (fun _a =>
                                  ‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                    ‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * _a)
                                (Eq.symm rfl)))
                            (Eq.refl
                              (‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                        (Mathlib.Tactic.Ring.Common.atom_pf ‖(ch.system.stepAt s w).output‖ rfl
                          (Eq.mpr
                            (id
                              (congrArg
                                (fun _a =>
                                  ‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                    ‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 * _a)
                                (Eq.symm rfl)))
                            (Eq.refl
                              (‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                        (Mathlib.Tactic.Ring.Common.sub_pf
                          (Mathlib.Tactic.Ring.Common.neg_add
                            (Mathlib.Tactic.Ring.Common.neg_mul ‖(ch.system.stepAt s w).output‖
                              (Nat.rawCast 1)
                              (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                                (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                                  (Mathlib.Meta.NormNum.IsNat.to_isInt
                                    (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                                  (Eq.refl (Int.negOfNat 1)))))
                            Mathlib.Tactic.Ring.Common.neg_zero)
                          (Mathlib.Tactic.Ring.Common.add_pf_add_lt
                            (‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)
                            (Mathlib.Tactic.Ring.Common.add_pf_zero_add
                              (‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 *
                                  (Int.negOfNat 1).rawCast +
                                0)))))
                      (Mathlib.Tactic.Ring.cast_zero
                        (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
                      (Mathlib.Tactic.Ring.Common.sub_pf Mathlib.Tactic.Ring.Common.neg_zero
                        (Mathlib.Tactic.Ring.Common.add_pf_add_zero
                          (‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 +
                            (‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 *
                                (Int.negOfNat 1).rawCast +
                              0)))))
                    (Mathlib.Tactic.Ring.Common.neg_add
                      (Mathlib.Tactic.Ring.Common.neg_mul ‖(ch.system.stepAt s w).input‖
                        (Nat.rawCast 1)
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt
                              (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      (Mathlib.Tactic.Ring.Common.neg_add
                        (Mathlib.Tactic.Ring.Common.neg_mul ‖(ch.system.stepAt s w).output‖
                          (Nat.rawCast 1)
                          (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                            (Mathlib.Meta.NormNum.IsInt.to_isNat
                              (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                                (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                                (Eq.refl (Int.ofNat 1))))))
                        Mathlib.Tactic.Ring.Common.neg_zero)))
                  (Mathlib.Tactic.Ring.Common.sub_congr
                    (Mathlib.Tactic.Ring.Common.sub_congr
                      (Mathlib.Tactic.Ring.Common.atom_pf
                        ‖{ current := s, input := w, next := (ch.component.1 s fun x => w).1,
                              output := (ch.component.1 s fun x => w).2 0,
                              holds := InformationSystem.stepAt._proof_1 ch.system s w }.input‖
                        rfl
                        (Eq.mpr
                          (id
                            (congrArg
                              (fun _a =>
                                ‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                  ‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * _a)
                              (Eq.symm rfl)))
                          (Eq.refl
                            (‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                      (Mathlib.Tactic.Ring.Common.atom_pf
                        ‖{ current := s, input := w, next := (ch.component.1 s fun x => w).1,
                              output := (ch.component.1 s fun x => w).2 0,
                              holds := InformationSystem.stepAt._proof_1 ch.system s w }.output‖
                        rfl
                        (Eq.mpr
                          (id
                            (congrArg
                              (fun _a =>
                                ‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                  ‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 * _a)
                              (Eq.symm rfl)))
                          (Eq.refl
                            (‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                      (Mathlib.Tactic.Ring.Common.sub_pf
                        (Mathlib.Tactic.Ring.Common.neg_add
                          (Mathlib.Tactic.Ring.Common.neg_mul ‖(ch.system.stepAt s w).output‖
                            (Nat.rawCast 1)
                            (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                              (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                                (Mathlib.Meta.NormNum.IsNat.to_isInt
                                  (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                                (Eq.refl (Int.negOfNat 1)))))
                          Mathlib.Tactic.Ring.Common.neg_zero)
                        (Mathlib.Tactic.Ring.Common.add_pf_add_lt
                          (‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)
                          (Mathlib.Tactic.Ring.Common.add_pf_zero_add
                            (‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 *
                                (Int.negOfNat 1).rawCast +
                              0)))))
                    (Mathlib.Tactic.Ring.Common.sub_congr
                      (Mathlib.Tactic.Ring.Common.atom_pf ‖(ch.component.1 s fun x => w).1‖ rfl
                        (Eq.mpr
                          (id
                            (congrArg
                              (fun _a =>
                                ‖(ch.component.1 s fun x => w).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                  ‖(ch.component.1 s fun x => w).1‖ ^ Nat.rawCast 1 * _a)
                              (Eq.symm rfl)))
                          (Eq.refl
                            (‖(ch.component.1 s fun x => w).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                      (Mathlib.Tactic.Ring.Common.atom_pf ‖s‖ rfl
                        (Eq.mpr
                          (id
                            (congrArg
                              (fun _a =>
                                ‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖s‖ ^ Nat.rawCast 1 * _a)
                              (Eq.symm rfl)))
                          (Eq.refl (‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                      (Mathlib.Tactic.Ring.Common.sub_pf
                        (Mathlib.Tactic.Ring.Common.neg_add
                          (Mathlib.Tactic.Ring.Common.neg_mul ‖s‖ (Nat.rawCast 1)
                            (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                              (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                                (Mathlib.Meta.NormNum.IsNat.to_isInt
                                  (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                                (Eq.refl (Int.negOfNat 1)))))
                          Mathlib.Tactic.Ring.Common.neg_zero)
                        (Mathlib.Tactic.Ring.Common.add_pf_add_lt
                          (‖(ch.component.1 s fun x => w).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1)
                          (Mathlib.Tactic.Ring.Common.add_pf_zero_add
                            (‖s‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                    (Mathlib.Tactic.Ring.Common.sub_pf
                      (Mathlib.Tactic.Ring.Common.neg_add
                        (Mathlib.Tactic.Ring.Common.neg_mul ‖(ch.component.1 s fun x => w).1‖
                          (Nat.rawCast 1)
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                              (Mathlib.Meta.NormNum.IsNat.to_isInt
                                (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                              (Eq.refl (Int.negOfNat 1)))))
                        (Mathlib.Tactic.Ring.Common.neg_add
                          (Mathlib.Tactic.Ring.Common.neg_mul ‖s‖ (Nat.rawCast 1)
                            (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                              (Mathlib.Meta.NormNum.IsInt.to_isNat
                                (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                                  (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                                  (Eq.refl (Int.ofNat 1))))))
                          Mathlib.Tactic.Ring.Common.neg_zero))
                      (Mathlib.Tactic.Ring.Common.add_pf_add_lt
                        (‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.Common.add_pf_add_lt
                          (‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 *
                            (Int.negOfNat 1).rawCast)
                          (Mathlib.Tactic.Ring.Common.add_pf_zero_add
                            (‖(ch.component.1 s fun x => w).1‖ ^ Nat.rawCast 1 *
                                (Int.negOfNat 1).rawCast +
                              (‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))))
                  (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖(ch.system.stepAt s w).input‖
                      (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                          (Mathlib.Meta.NormNum.IsNat.to_isInt
                            (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                          (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero
                      (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero
                        ‖(ch.system.stepAt s w).output‖ (Nat.rawCast 1)
                        (Mathlib.Meta.NormNum.IsInt.to_isNat
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt
                              (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                            (Eq.refl (Int.ofNat 0)))))
                      (Mathlib.Tactic.Ring.Common.add_pf_zero_add
                        (‖(ch.component.1 s fun x => w).1‖ ^ Nat.rawCast 1 *
                            (Int.negOfNat 1).rawCast +
                          (‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))))
                (Mathlib.Tactic.Ring.Common.sub_congr
                  (Mathlib.Tactic.Ring.Common.atom_pf ‖(ch.system.step s w).1‖ rfl
                    (Eq.mpr
                      (id
                        (congrArg
                          (fun _a =>
                            ‖(ch.component.1 s fun x => w).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 =
                              ‖(ch.component.1 s fun x => w).1‖ ^ Nat.rawCast 1 * _a)
                          (Eq.symm rfl)))
                      (Eq.refl
                        (‖(ch.component.1 s fun x => w).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                  (Mathlib.Tactic.Ring.Common.atom_pf ‖s‖ rfl
                    (Eq.mpr
                      (id
                        (congrArg
                          (fun _a => ‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖s‖ ^ Nat.rawCast 1 * _a)
                          (Eq.symm rfl)))
                      (Eq.refl (‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                  (Mathlib.Tactic.Ring.Common.sub_pf
                    (Mathlib.Tactic.Ring.Common.neg_add
                      (Mathlib.Tactic.Ring.Common.neg_mul ‖s‖ (Nat.rawCast 1)
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt
                              (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.Common.neg_zero)
                    (Mathlib.Tactic.Ring.Common.add_pf_add_lt
                      (‖(ch.component.1 s fun x => w).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1)
                      (Mathlib.Tactic.Ring.Common.add_pf_zero_add
                        (‖s‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero
                  (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖(ch.component.1 s fun x => w).1‖
                    (Nat.rawCast 1)
                    (Mathlib.Meta.NormNum.IsInt.to_isNat
                      (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                        (Mathlib.Meta.NormNum.IsNat.to_isInt
                          (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                        (Eq.refl (Int.ofNat 0)))))
                  (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖s‖ (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsNat.to_isInt
                            (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                          (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.Common.add_pf_zero_add 0))))
              (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
          (Mathlib.Tactic.Linarith.lt_of_eq_of_lt
            (Mathlib.Tactic.Linarith.eq_of_eq_of_eq (neg_eq_zero.mpr (sub_eq_zero_of_eq h))
              (sub_eq_zero_of_eq this))
            (Mathlib.Tactic.Linarith.sub_neg_of_lt a))))
    (Not.intro fun a =>
      Mathlib.Tactic.Linarith.lt_irrefl
        (Eq.mp
          (congrArg (fun _a => _a < 0)
            (Mathlib.Tactic.Ring.of_eq
              (Mathlib.Tactic.Ring.Common.add_congr
                (Mathlib.Tactic.Ring.Common.add_congr
                  (Mathlib.Tactic.Ring.Common.sub_congr
                    (Mathlib.Tactic.Ring.Common.sub_congr
                      (Mathlib.Tactic.Ring.Common.atom_pf ‖(ch.system.stepAt s w).input‖ rfl
                        (Eq.mpr
                          (id
                            (congrArg
                              (fun _a =>
                                ‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                  ‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * _a)
                              (Eq.symm rfl)))
                          (Eq.refl
                            (‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                      (Mathlib.Tactic.Ring.Common.atom_pf ‖(ch.system.stepAt s w).output‖ rfl
                        (Eq.mpr
                          (id
                            (congrArg
                              (fun _a =>
                                ‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                  ‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 * _a)
                              (Eq.symm rfl)))
                          (Eq.refl
                            (‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                      (Mathlib.Tactic.Ring.Common.sub_pf
                        (Mathlib.Tactic.Ring.Common.neg_add
                          (Mathlib.Tactic.Ring.Common.neg_mul ‖(ch.system.stepAt s w).output‖
                            (Nat.rawCast 1)
                            (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                              (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                                (Mathlib.Meta.NormNum.IsNat.to_isInt
                                  (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                                (Eq.refl (Int.negOfNat 1)))))
                          Mathlib.Tactic.Ring.Common.neg_zero)
                        (Mathlib.Tactic.Ring.Common.add_pf_add_lt
                          (‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)
                          (Mathlib.Tactic.Ring.Common.add_pf_zero_add
                            (‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 *
                                (Int.negOfNat 1).rawCast +
                              0)))))
                    (Mathlib.Tactic.Ring.cast_zero
                      (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
                    (Mathlib.Tactic.Ring.Common.sub_pf Mathlib.Tactic.Ring.Common.neg_zero
                      (Mathlib.Tactic.Ring.Common.add_pf_add_zero
                        (‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 +
                          (‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 *
                              (Int.negOfNat 1).rawCast +
                            0)))))
                  (Mathlib.Tactic.Ring.Common.neg_congr
                    (Mathlib.Tactic.Ring.Common.sub_congr
                      (Mathlib.Tactic.Ring.Common.sub_congr
                        (Mathlib.Tactic.Ring.Common.atom_pf
                          ‖{ current := s, input := w, next := (ch.component.1 s fun x => w).1,
                                output := (ch.component.1 s fun x => w).2 0,
                                holds := InformationSystem.stepAt._proof_1 ch.system s w }.input‖
                          rfl
                          (Eq.mpr
                            (id
                              (congrArg
                                (fun _a =>
                                  ‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                    ‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * _a)
                                (Eq.symm rfl)))
                            (Eq.refl
                              (‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                        (Mathlib.Tactic.Ring.Common.atom_pf
                          ‖{ current := s, input := w, next := (ch.component.1 s fun x => w).1,
                                output := (ch.component.1 s fun x => w).2 0,
                                holds := InformationSystem.stepAt._proof_1 ch.system s w }.output‖
                          rfl
                          (Eq.mpr
                            (id
                              (congrArg
                                (fun _a =>
                                  ‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                    ‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 * _a)
                                (Eq.symm rfl)))
                            (Eq.refl
                              (‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                        (Mathlib.Tactic.Ring.Common.sub_pf
                          (Mathlib.Tactic.Ring.Common.neg_add
                            (Mathlib.Tactic.Ring.Common.neg_mul ‖(ch.system.stepAt s w).output‖
                              (Nat.rawCast 1)
                              (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                                (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                                  (Mathlib.Meta.NormNum.IsNat.to_isInt
                                    (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                                  (Eq.refl (Int.negOfNat 1)))))
                            Mathlib.Tactic.Ring.Common.neg_zero)
                          (Mathlib.Tactic.Ring.Common.add_pf_add_lt
                            (‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)
                            (Mathlib.Tactic.Ring.Common.add_pf_zero_add
                              (‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 *
                                  (Int.negOfNat 1).rawCast +
                                0)))))
                      (Mathlib.Tactic.Ring.Common.sub_congr
                        (Mathlib.Tactic.Ring.Common.atom_pf ‖(ch.component.1 s fun x => w).1‖ rfl
                          (Eq.mpr
                            (id
                              (congrArg
                                (fun _a =>
                                  ‖(ch.component.1 s fun x => w).1‖ ^ Nat.rawCast 1 *
                                      Nat.rawCast 1 =
                                    ‖(ch.component.1 s fun x => w).1‖ ^ Nat.rawCast 1 * _a)
                                (Eq.symm rfl)))
                            (Eq.refl
                              (‖(ch.component.1 s fun x => w).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                        (Mathlib.Tactic.Ring.Common.atom_pf ‖s‖ rfl
                          (Eq.mpr
                            (id
                              (congrArg
                                (fun _a =>
                                  ‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖s‖ ^ Nat.rawCast 1 * _a)
                                (Eq.symm rfl)))
                            (Eq.refl (‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                        (Mathlib.Tactic.Ring.Common.sub_pf
                          (Mathlib.Tactic.Ring.Common.neg_add
                            (Mathlib.Tactic.Ring.Common.neg_mul ‖s‖ (Nat.rawCast 1)
                              (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                                (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                                  (Mathlib.Meta.NormNum.IsNat.to_isInt
                                    (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                                  (Eq.refl (Int.negOfNat 1)))))
                            Mathlib.Tactic.Ring.Common.neg_zero)
                          (Mathlib.Tactic.Ring.Common.add_pf_add_lt
                            (‖(ch.component.1 s fun x => w).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1)
                            (Mathlib.Tactic.Ring.Common.add_pf_zero_add
                              (‖s‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                      (Mathlib.Tactic.Ring.Common.sub_pf
                        (Mathlib.Tactic.Ring.Common.neg_add
                          (Mathlib.Tactic.Ring.Common.neg_mul ‖(ch.component.1 s fun x => w).1‖
                            (Nat.rawCast 1)
                            (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                              (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                                (Mathlib.Meta.NormNum.IsNat.to_isInt
                                  (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                                (Eq.refl (Int.negOfNat 1)))))
                          (Mathlib.Tactic.Ring.Common.neg_add
                            (Mathlib.Tactic.Ring.Common.neg_mul ‖s‖ (Nat.rawCast 1)
                              (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                                (Mathlib.Meta.NormNum.IsInt.to_isNat
                                  (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                                    (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                                    (Eq.refl (Int.ofNat 1))))))
                            Mathlib.Tactic.Ring.Common.neg_zero))
                        (Mathlib.Tactic.Ring.Common.add_pf_add_lt
                          (‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)
                          (Mathlib.Tactic.Ring.Common.add_pf_add_lt
                            (‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 *
                              (Int.negOfNat 1).rawCast)
                            (Mathlib.Tactic.Ring.Common.add_pf_zero_add
                              (‖(ch.component.1 s fun x => w).1‖ ^ Nat.rawCast 1 *
                                  (Int.negOfNat 1).rawCast +
                                (‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))))
                    (Mathlib.Tactic.Ring.Common.neg_add
                      (Mathlib.Tactic.Ring.Common.neg_mul ‖(ch.system.stepAt s w).input‖
                        (Nat.rawCast 1)
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt
                              (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      (Mathlib.Tactic.Ring.Common.neg_add
                        (Mathlib.Tactic.Ring.Common.neg_mul ‖(ch.system.stepAt s w).output‖
                          (Nat.rawCast 1)
                          (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                            (Mathlib.Meta.NormNum.IsInt.to_isNat
                              (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                                (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                                (Eq.refl (Int.ofNat 1))))))
                        (Mathlib.Tactic.Ring.Common.neg_add
                          (Mathlib.Tactic.Ring.Common.neg_mul ‖(ch.component.1 s fun x => w).1‖
                            (Nat.rawCast 1)
                            (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                              (Mathlib.Meta.NormNum.IsInt.to_isNat
                                (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                                  (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                                  (Eq.refl (Int.ofNat 1))))))
                          (Mathlib.Tactic.Ring.Common.neg_add
                            (Mathlib.Tactic.Ring.Common.neg_mul ‖s‖ (Nat.rawCast 1)
                              (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                                (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                                  (Mathlib.Meta.NormNum.IsNat.to_isInt
                                    (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                                  (Eq.refl (Int.negOfNat 1)))))
                            Mathlib.Tactic.Ring.Common.neg_zero)))))
                  (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖(ch.system.stepAt s w).input‖
                      (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsNat.to_isInt
                            (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                          (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero
                      (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero
                        ‖(ch.system.stepAt s w).output‖ (Nat.rawCast 1)
                        (Mathlib.Meta.NormNum.IsInt.to_isNat
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt
                              (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                            (Eq.refl (Int.ofNat 0)))))
                      (Mathlib.Tactic.Ring.Common.add_pf_zero_add
                        (‖(ch.component.1 s fun x => w).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 +
                          (‖s‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))))
                (Mathlib.Tactic.Ring.Common.sub_congr
                  (Mathlib.Tactic.Ring.Common.atom_pf ‖s‖ rfl
                    (Eq.mpr
                      (id
                        (congrArg
                          (fun _a => ‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖s‖ ^ Nat.rawCast 1 * _a)
                          (Eq.symm rfl)))
                      (Eq.refl (‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                  (Mathlib.Tactic.Ring.Common.atom_pf ‖(ch.system.step s w).1‖ rfl
                    (Eq.mpr
                      (id
                        (congrArg
                          (fun _a =>
                            ‖(ch.component.1 s fun x => w).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 =
                              ‖(ch.component.1 s fun x => w).1‖ ^ Nat.rawCast 1 * _a)
                          (Eq.symm rfl)))
                      (Eq.refl
                        (‖(ch.component.1 s fun x => w).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                  (Mathlib.Tactic.Ring.Common.sub_pf
                    (Mathlib.Tactic.Ring.Common.neg_add
                      (Mathlib.Tactic.Ring.Common.neg_mul ‖(ch.component.1 s fun x => w).1‖
                        (Nat.rawCast 1)
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt
                              (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.Common.neg_zero)
                    (Mathlib.Tactic.Ring.Common.add_pf_add_gt
                      (‖(ch.component.1 s fun x => w).1‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)
                      (Mathlib.Tactic.Ring.Common.add_pf_add_zero
                        (‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero
                  (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖(ch.component.1 s fun x => w).1‖
                    (Nat.rawCast 1)
                    (Mathlib.Meta.NormNum.IsInt.to_isNat
                      (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                        (Mathlib.Meta.NormNum.IsNat.to_isInt
                          (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                        (Eq.refl (Int.ofNat 0)))))
                  (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖s‖ (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                          (Mathlib.Meta.NormNum.IsNat.to_isInt
                            (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                          (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.Common.add_pf_zero_add 0))))
              (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
          (Mathlib.Tactic.Linarith.lt_of_eq_of_lt
            (Mathlib.Tactic.Linarith.eq_of_eq_of_eq (sub_eq_zero_of_eq h)
              (neg_eq_zero.mpr (sub_eq_zero_of_eq this)))
            (Mathlib.Tactic.Linarith.sub_neg_of_lt a))))

Complexity: 125240 (size of the value term)

Dependencies: Channel, Channel.lossless, Channel.system

Proof dependencies: Channel.loss, InformationSystem.Step.delta, InformationSystem.Step.delta_alt, InformationSystem.stepAt

Mathlib dependencies: Int.rawCast, Mathlib.Meta.NormNum.IsInt.of_raw, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.IsNat.of_raw, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Meta.NormNum.isInt_add, Mathlib.Meta.NormNum.isInt_neg, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Linarith.eq_of_eq_of_eq, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Mathlib.Tactic.Linarith.lt_of_eq_of_lt, Mathlib.Tactic.Linarith.sub_neg_of_lt, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.add_overlap_pf_zero, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_lt, Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.atom_pf, Mathlib.Tactic.Ring.Common.neg_add, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.Common.neg_mul, Mathlib.Tactic.Ring.Common.neg_zero, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.sub_pf, Mathlib.Tactic.Ring.cast_zero, Mathlib.Tactic.Ring.of_eq, Nat.cast_zero, Nat.rawCast, Norm, Real, Ring, neg_eq_zero, sub_eq_zero_of_eq

Lean core dependencies: Eq, Eq.mp, Eq.mpr, Eq.symm, Fin, Int, Int.negOfNat, Nat, Nonempty, Not.intro, congrArg, id, inferInstance, rfl

Used by: (none)

theorem Channel.lossy_loses_overall {State Wire : Type} [Nonempty State] [Norm State] [Nonempty Wire]
  [Norm Wire] (ch : Channel State Wire) (s : State) (w : Wire) (hloss : ch.loss s w > 0) :
  ∃ ws, ws.totalSize > (ch.system.eval s ws).2.totalSize
Show details 
fun {State Wire} [Nonempty State] [Norm State] [Nonempty Wire] [Norm Wire] ch s w hloss =>
  Exists.intro [w]
    (Eq.mpr
      (id
        (congr (congrArg GT.gt (add_zero ‖w‖))
          (Eq.trans
            (congrArg List.sum
              (List.map.eq_2 (fun x => ‖x‖) ((ch.component.1 s fun x => w).2 0) []))
            (add_zero ‖(ch.component.1 s fun x => w).2 0‖))))
      (have this := rfl;
      lt_of_not_ge fun a =>
        Mathlib.Tactic.Linarith.lt_irrefl
          (Eq.mp
            (congrArg (fun _a => _a < 0)
              (Mathlib.Tactic.Ring.of_eq
                (Mathlib.Tactic.Ring.Common.add_congr
                  (Mathlib.Tactic.Ring.Common.sub_congr
                    (Mathlib.Tactic.Ring.cast_zero
                      (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
                    (Mathlib.Tactic.Ring.Common.sub_congr
                      (Mathlib.Tactic.Ring.Common.atom_pf ‖(ch.system.stepAt s w).input‖ rfl
                        (Eq.mpr
                          (id
                            (congrArg
                              (fun _a =>
                                ‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                  ‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * _a)
                              (Eq.symm rfl)))
                          (Eq.refl
                            (‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                      (Mathlib.Tactic.Ring.Common.atom_pf ‖(ch.system.stepAt s w).output‖ rfl
                        (Eq.mpr
                          (id
                            (congrArg
                              (fun _a =>
                                ‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                  ‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 * _a)
                              (Eq.symm rfl)))
                          (Eq.refl
                            (‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                      (Mathlib.Tactic.Ring.Common.sub_pf
                        (Mathlib.Tactic.Ring.Common.neg_add
                          (Mathlib.Tactic.Ring.Common.neg_mul ‖(ch.system.stepAt s w).output‖
                            (Nat.rawCast 1)
                            (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                              (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                                (Mathlib.Meta.NormNum.IsNat.to_isInt
                                  (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                                (Eq.refl (Int.negOfNat 1)))))
                          Mathlib.Tactic.Ring.Common.neg_zero)
                        (Mathlib.Tactic.Ring.Common.add_pf_add_lt
                          (‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)
                          (Mathlib.Tactic.Ring.Common.add_pf_zero_add
                            (‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 *
                                (Int.negOfNat 1).rawCast +
                              0)))))
                    (Mathlib.Tactic.Ring.Common.sub_pf
                      (Mathlib.Tactic.Ring.Common.neg_add
                        (Mathlib.Tactic.Ring.Common.neg_mul ‖(ch.system.stepAt s w).input‖
                          (Nat.rawCast 1)
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                              (Mathlib.Meta.NormNum.IsNat.to_isInt
                                (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                              (Eq.refl (Int.negOfNat 1)))))
                        (Mathlib.Tactic.Ring.Common.neg_add
                          (Mathlib.Tactic.Ring.Common.neg_mul ‖(ch.system.stepAt s w).output‖
                            (Nat.rawCast 1)
                            (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                              (Mathlib.Meta.NormNum.IsInt.to_isNat
                                (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                                  (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                                  (Eq.refl (Int.ofNat 1))))))
                          Mathlib.Tactic.Ring.Common.neg_zero))
                      (Mathlib.Tactic.Ring.Common.add_pf_zero_add
                        (‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast +
                          (‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                  (Mathlib.Tactic.Ring.Common.sub_congr
                    (Mathlib.Tactic.Ring.Common.atom_pf ‖w‖ rfl
                      (Eq.mpr
                        (id
                          (congrArg
                            (fun _a =>
                              ‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                ‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * _a)
                            (Eq.symm rfl)))
                        (Eq.refl (‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                    (Mathlib.Tactic.Ring.Common.atom_pf ‖(ch.component.1 s fun x => w).2 0‖ rfl
                      (Eq.mpr
                        (id
                          (congrArg
                            (fun _a =>
                              ‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                ‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 * _a)
                            (Eq.symm rfl)))
                        (Eq.refl
                          (‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 * Nat.rawCast 1))))
                    (Mathlib.Tactic.Ring.Common.sub_pf
                      (Mathlib.Tactic.Ring.Common.neg_add
                        (Mathlib.Tactic.Ring.Common.neg_mul ‖(ch.system.stepAt s w).output‖
                          (Nat.rawCast 1)
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                              (Mathlib.Meta.NormNum.IsNat.to_isInt
                                (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                              (Eq.refl (Int.negOfNat 1)))))
                        Mathlib.Tactic.Ring.Common.neg_zero)
                      (Mathlib.Tactic.Ring.Common.add_pf_add_lt
                        (‖(ch.system.stepAt s w).input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.Common.add_pf_zero_add
                          (‖(ch.system.stepAt s w).output‖ ^ Nat.rawCast 1 *
                              (Int.negOfNat 1).rawCast +
                            0)))))
                  (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖(ch.system.stepAt s w).input‖
                      (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                          (Mathlib.Meta.NormNum.IsNat.to_isInt
                            (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                          (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero
                      (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero
                        ‖(ch.system.stepAt s w).output‖ (Nat.rawCast 1)
                        (Mathlib.Meta.NormNum.IsInt.to_isNat
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt
                              (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                            (Eq.refl (Int.ofNat 0)))))
                      (Mathlib.Tactic.Ring.Common.add_pf_zero_add 0))))
                (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
            (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
              (Mathlib.Tactic.Linarith.sub_neg_of_lt hloss)
              (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)))))

Complexity: 29666 (size of the value term)

Dependencies: Channel, Channel.loss, Channel.system, InformationSystem.eval, List.totalSize

Proof dependencies: InformationSystem.stepAt

Mathlib dependencies: Int.rawCast, Mathlib.Meta.NormNum.IsInt.of_raw, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.IsNat.of_raw, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Meta.NormNum.isInt_add, Mathlib.Meta.NormNum.isInt_neg, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Linarith.add_lt_of_neg_of_le, Mathlib.Tactic.Linarith.lt_irrefl, Mathlib.Tactic.Linarith.sub_neg_of_lt, Mathlib.Tactic.Linarith.sub_nonpos_of_le, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.add_overlap_pf_zero, Mathlib.Tactic.Ring.Common.add_pf_add_lt, Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.atom_pf, Mathlib.Tactic.Ring.Common.neg_add, Mathlib.Tactic.Ring.Common.neg_mul, Mathlib.Tactic.Ring.Common.neg_zero, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.sub_pf, Mathlib.Tactic.Ring.cast_zero, Mathlib.Tactic.Ring.of_eq, Nat.cast_zero, Nat.rawCast, Norm, Real, Ring, add_zero, lt_of_not_ge

Lean core dependencies: Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, Exists, Fin, GT.gt, Int, Int.negOfNat, List, List.map, List.sum, Nat, Nonempty, congr, congrArg, id, inferInstance, rfl

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitionabbreviationtheoremdeclared elsewheredependencyproof dependency
legend