aggregateThroughput_succ

formal source

  55theorem aggregateThroughput_zero : aggregateThroughput 0 = 0 := by
  56  unfold aggregateThroughput; simp
  57
  58theorem aggregateThroughput_succ (N : ℕ) :
  59    aggregateThroughput (N + 1) = aggregateThroughput N + T_node := by
  60  unfold aggregateThroughput; push_cast; ring
  61
  62theorem aggregateThroughput_pos {N : ℕ} (h : 1 ≤ N) :
  63    0 < aggregateThroughput N := by
  64  unfold aggregateThroughput
  65  exact mul_pos (by exact_mod_cast (by omega : 0 < N)) T_node_pos
  66
  67theorem aggregateThroughput_strict_mono {N M : ℕ} (h : N < M) :
  68    aggregateThroughput N < aggregateThroughput M := by
  69  unfold aggregateThroughput
  70  have h_real : (N : ℝ) < (M : ℝ) := by exact_mod_cast h
  71  exact (mul_lt_mul_iff_of_pos_right T_node_pos).mpr h_real
  72
  73/-- Linearity: throughput at 2N is exactly twice throughput at N. -/
  74theorem aggregateThroughput_double (N : ℕ) :
  75    aggregateThroughput (2 * N) = 2 * aggregateThroughput N := by
  76  unfold aggregateThroughput; push_cast; ring
  77
  78/-! ## §3. Distance-decoupled latency -/
  79
  80/-- Distance-decoupled latency: returns `latency_per_pair` regardless
  81of node-pair separation `d`. -/
  82def pairwiseLatency (d : ℝ) : ℝ := latency_per_pair
  83
  84theorem pairwiseLatency_constant (d₁ d₂ : ℝ) :
  85    pairwiseLatency d₁ = pairwiseLatency d₂ := rfl
  86
  87theorem pairwiseLatency_pos (d : ℝ) : 0 < pairwiseLatency d :=
  88  latency_per_pair_pos