perturbation_cost_small_bound

formal source

 255    0 < Jcost (1 + ε) := by
 256  exact Jcost_pos_of_ne_one (1 + ε) hε_pos (by intro h; exact hε (by linarith))
 257
 258theorem perturbation_cost_small_bound (ε : ℝ) (hε : |ε| ≤ 1 / 10) :
 259    |Jcost (1 + ε) - ε ^ 2 / 2| ≤ ε ^ 2 / 10 :=
 260  Jcost_small_strain_bound ε hε
 261
 262/-! ## Part VIII: The d'Alembert Cascade -/
 263
 264theorem dalembert_cascade (a b : ℤ) :
 265    Jcost (PhiForcing.φ ^ a * PhiForcing.φ ^ b) +
 266    Jcost (PhiForcing.φ ^ a / PhiForcing.φ ^ b) =
 267    2 * Jcost (PhiForcing.φ ^ a) + 2 * Jcost (PhiForcing.φ ^ b) +
 268    2 * Jcost (PhiForcing.φ ^ a) * Jcost (PhiForcing.φ ^ b) :=
 269  dalembert_identity (zpow_pos PhiForcing.phi_pos a) (zpow_pos PhiForcing.phi_pos b)
 270
 271theorem phi_power_compose (a b : ℤ) :
 272    PhiForcing.φ ^ a * PhiForcing.φ ^ b = PhiForcing.φ ^ (a + b) :=
 273  (zpow_add₀ PhiForcing.phi_pos.ne' a b).symm
 274
 275theorem phi_power_ratio (a b : ℤ) :
 276    PhiForcing.φ ^ a / PhiForcing.φ ^ b = PhiForcing.φ ^ (a - b) := by
 277  rw [div_eq_mul_inv, ← zpow_neg, ← zpow_add₀ PhiForcing.phi_pos.ne', sub_eq_add_neg]
 278
 279theorem ladder_cascade_bound (a b : ℤ) :
 280    Jcost (phi_ladder (a + b)) ≤
 281    2 * Jcost (phi_ladder a) + 2 * Jcost (phi_ladder b) +
 282    2 * Jcost (phi_ladder a) * Jcost (phi_ladder b) := by
 283  unfold phi_ladder
 284  rw [← phi_power_compose]
 285  exact Jcost_submult (zpow_pos PhiForcing.phi_pos a) (zpow_pos PhiForcing.phi_pos b)
 286
 287theorem doubling_cascade (n : ℤ) (_hn : n ≠ 0) :
 288    Jcost (phi_ladder (2 * n)) =