postingStep_of_monotone_and_ledgerJlogCost_le_Jlog1

proof body

Tactic-mode proof.

 255    (hneq : L ≠ L')
 256    (hle : ledgerJlogCost (d := d) L L' ≤ Cost.Jlog (1 : ℝ)) :
 257    PostingStep (d := d) L L' := by
 258  classical
 259  -- helper: deltas
 260  let dΔ : Fin d → ℤ := fun i => L'.debit i - L.debit i
 261  let cΔ : Fin d → ℤ := fun i => L'.credit i - L.credit i
 262  have hdNonneg : ∀ i : Fin d, 0 ≤ dΔ i := by
 263    intro i
 264    have : L.debit i ≤ L'.debit i := hmono.1 i
 265    dsimp [dΔ]
 266    linarith
 267  have hcNonneg : ∀ i : Fin d, 0 ≤ cΔ i := by
 268    intro i
 269    have : L.credit i ≤ L'.credit i := hmono.2 i
 270    dsimp [cΔ]
 271    linarith
 272
 273  -- show every delta is ≤ 1 (otherwise cost would exceed Jlog 1)
 274  have hdLeOne : ∀ i : Fin d, dΔ i ≤ 1 := by
 275    intro i
 276    by_contra hgt
 277    have hlt : (1 : ℤ) < dΔ i := lt_of_not_ge hgt
 278    have h2 : (2 : ℤ) ≤ dΔ i := by
 279      -- `2 ≤ z ↔ 1 < z`
 280      exact (Int.add_one_le_iff).2 hlt
 281    -- strict lower bound on this term
 282    have hx : (1 : ℝ) < ((dΔ i : ℤ) : ℝ) := by
 283      -- cast `1 < dΔ i` to ℝ
 284      exact_mod_cast hlt
 285    have hterm_lt : Cost.Jlog (1 : ℝ) < Cost.Jlog ((dΔ i : ℤ) : ℝ) :=
 286      jlog_lt_jlog_of_one_lt (x := ((dΔ i : ℤ) : ℝ)) hx
 287    -- this term is bounded by total cost (single term ≤ sum) and total cost ≤ Jlog 1: contradiction
 288    let fD : Fin d → ℝ := fun j => Cost.Jlog ((dΔ j : ℤ) : ℝ)
 289    have hterm_le_sum : fD i ≤ ∑ j : Fin d, fD j := by
 290      -- `fD i ≤ sum univ fD` by nonneg
 291      have hnonneg : ∀ j : Fin d, 0 ≤ fD j := fun _ => Cost.Jlog_nonneg _
 292      -- use `i` in univ
 293      -- work directly with `Finset.univ` to avoid rewriting via `Fintype.sum`
 294      have : fD i ≤ Finset.sum (Finset.univ : Finset (Fin d)) fD :=
 295        Finset.single_le_sum (by
 296          intro j hj
 297          exact hnonneg j) (by simp : i ∈ (Finset.univ : Finset (Fin d)))
 298      simpa using this
 299    have hsum_le_cost : (∑ j : Fin d, fD j) ≤ ledgerJlogCost (d := d) L L' := by
 300      -- debit sum ≤ debit sum + credit sum
 301      have hcredit_nonneg : 0 ≤ ∑ j : Fin d, Cost.Jlog ((cΔ j : ℤ) : ℝ) :=
 302        Finset.sum_nonneg (fun _ _ => Cost.Jlog_nonneg _)
 303      dsimp [ledgerJlogCost, dΔ, cΔ]
 304      exact le_add_of_nonneg_right hcredit_nonneg
 305    have hterm_le_cost : Cost.Jlog ((dΔ i : ℤ) : ℝ) ≤ ledgerJlogCost (d := d) L L' := by
 306      -- rewrite `fD i` and compose inequalities
 307      have : fD i ≤ ledgerJlogCost (d := d) L L' := le_trans hterm_le_sum hsum_le_cost
 308      simpa [fD] using this
 309    have : Cost.Jlog (1 : ℝ) < ledgerJlogCost (d := d) L L' :=
 310      lt_of_lt_of_le hterm_lt hterm_le_cost
 311    exact (not_lt_of_ge hle) this
 312
 313  have hcLeOne : ∀ i : Fin d, cΔ i ≤ 1 := by
 314    intro i
 315    by_contra hgt
 316    have hlt : (1 : ℤ) < cΔ i := lt_of_not_ge hgt
 317    have hx : (1 : ℝ) < ((cΔ i : ℤ) : ℝ) := by exact_mod_cast hlt
 318    have hterm_lt : Cost.Jlog (1 : ℝ) < Cost.Jlog ((cΔ i : ℤ) : ℝ) :=
 319      jlog_lt_jlog_of_one_lt (x := ((cΔ i : ℤ) : ℝ)) hx
 320    let fC : Fin d → ℝ := fun j => Cost.Jlog ((cΔ j : ℤ) : ℝ)
 321    have hterm_le_sum : fC i ≤ ∑ j : Fin d, fC j := by
 322      have hnonneg : ∀ j : Fin d, 0 ≤ fC j := fun _ => Cost.Jlog_nonneg _
 323      have : fC i ≤ Finset.sum (Finset.univ : Finset (Fin d)) fC :=
 324        Finset.single_le_sum (by
 325          intro j hj
 326          exact hnonneg j) (by simp : i ∈ (Finset.univ : Finset (Fin d)))
 327      simpa using this
 328    have hsum_le_cost : (∑ j : Fin d, fC j) ≤ ledgerJlogCost (d := d) L L' := by
 329      have hdebit_nonneg : 0 ≤ ∑ j : Fin d, Cost.Jlog ((dΔ j : ℤ) : ℝ) :=
 330        Finset.sum_nonneg (fun _ _ => Cost.Jlog_nonneg _)
 331      dsimp [ledgerJlogCost, dΔ, cΔ]
 332      exact le_add_of_nonneg_left hdebit_nonneg
 333    have hterm_le_cost : Cost.Jlog ((cΔ i : ℤ) : ℝ) ≤ ledgerJlogCost (d := d) L L' := by
 334      have : fC i ≤ ledgerJlogCost (d := d) L L' := le_trans hterm_le_sum hsum_le_cost
 335-- ... 277 more lines elided ...