viscousRate

formal source

  50
  51Pure real arithmetic: if mu * h^2 <= nu then mu <= nu / h^2. -/
  52
  53def viscousRate (nu h : ℝ) : ℝ := nu / h ^ 2
  54
  55theorem viscous_dominates_of_product_bound
  56    {nu h mu : ℝ} (hh : 0 < h) (hbound : mu * h ^ 2 ≤ nu) :
  57    mu ≤ viscousRate nu h := by
  58  unfold viscousRate
  59  have hh2 : (0 : ℝ) < h ^ 2 := by positivity
  60  rwa [le_div_iff₀ hh2]
  61
  62/-! ## Gap 3: Sub-Kolmogorov Pair-Budget Absorption (PROVED)
  63
  64### Algebraic core: exact formula for J(1+eps)
  65
  66From J(x) = 1/2*(x + x^{-1}) - 1, for x = 1 + eps with eps >= 0:
  67
  68  J(1+eps) = eps^2 / (2*(1+eps))
  69
  70This is an exact algebraic identity from [P2]. -/
  71
  72theorem Jcost_one_plus_eps {eps : ℝ} (heps : 0 ≤ eps) :
  73    Jcost (1 + eps) = eps ^ 2 / (2 * (1 + eps)) := by
  74  unfold Jcost
  75  have hne : (1 : ℝ) + eps ≠ 0 := by linarith
  76  field_simp [hne]; ring
  77
  78/-- J(1+eps) <= eps^2/2 for eps >= 0.
  79
  80Proof: eps^2/(2*(1+eps)) <= eps^2/2 because 1+eps >= 1 and the numerator
  81is nonneg. -/
  82theorem Jcost_one_plus_eps_le_sq {eps : ℝ} (heps : 0 ≤ eps) :
  83    Jcost (1 + eps) ≤ eps ^ 2 / 2 := by