strictConcaveOn_gapR_Ici

proof body

Tactic-mode proof.

 111  -- Reduce to strict concavity of `Real.log` on `(0,∞)` and use an injective affine reparametrization.
 112  let g : ℝ → ℝ := Real.log
 113  have hlog : StrictConcaveOn ℝ (Set.Ioi (0 : ℝ)) g := strictConcaveOn_log_Ioi
 114
 115  have hφpos : 0 < phi := phi_pos
 116  have hφne : (phi : ℝ) ≠ 0 := ne_of_gt hφpos
 117  have hlogφpos : 0 < Real.log phi := Real.log_pos one_lt_phi
 118  have hlogφne : Real.log phi ≠ 0 := ne_of_gt hlogφpos
 119
 120  -- affine map h(x) = 1 + x/phi
 121  let hlin : ℝ →ₗ[ℝ] ℝ := (LinearMap.id : ℝ →ₗ[ℝ] ℝ).smulRight (1 / phi)
 122  let h : ℝ →ᵃ[ℝ] ℝ :=
 123    AffineMap.mk (toFun := fun x => 1 + x / phi) (linear := hlin) (map_vadd' := by
 124      intro p v
 125      -- v +ᵥ p = v + p in ℝ-torsor
 126      simp [hlin, add_div, hφne]
 127      ring)
 128
 129  -- helper: h maps Ici 0 into Ioi 0
 130  have h_img0 : ∀ {x : ℝ}, x ∈ Set.Ici (0 : ℝ) → h x ∈ Set.Ioi (0 : ℝ) := by
 131    intro x hx
 132    have hx0 : 0 ≤ x := hx
 133    have hx_div : 0 ≤ x / phi := div_nonneg hx0 (le_of_lt hφpos)
 134    have : (0 : ℝ) < 1 + x / phi := by linarith
 135    simpa [h] using this
 136
 137  -- injectivity of h on Ici 0
 138  have h_inj : Set.InjOn h (Set.Ici (0 : ℝ)) := by
 139    intro x hx y hy hxy
 140    have hEq : (1 + x / phi) = (1 + y / phi) := by simpa [h] using hxy
 141    have hDiv : x / phi = y / phi := by
 142      have h' := congrArg (fun t => t - 1) hEq
 143      simpa using h'
 144    have hm : (x / phi) * phi = (y / phi) * phi := congrArg (fun t => t * phi) hDiv
 145    simpa [div_eq_mul_inv, hφne, mul_assoc] using hm
 146
 147  -- strict concavity of log ∘ h on Ici 0
 148  have h_log_comp : StrictConcaveOn ℝ (Set.Ici (0 : ℝ)) (g ∘ h) := by
 149    refine ⟨convex_Ici (0 : ℝ), ?_⟩
 150    intro x hx y hy hxy a b ha hb hab
 151    have hx' : h x ∈ Set.Ioi (0 : ℝ) := h_img0 hx
 152    have hy' : h y ∈ Set.Ioi (0 : ℝ) := h_img0 hy
 153    have hxy' : h x ≠ h y := by
 154      intro hEq
 155      exact hxy (h_inj hx hy hEq)
 156    have hh : a * h x + b * h y = h (a * x + b * y) := by
 157      simpa [smul_eq_mul] using (Convex.combo_affine_apply (f := h) hab).symm
 158    -- Apply strict concavity of log and rewrite via hh
 159    have h0 := hlog.2 hx' hy' hxy' ha hb hab
 160    -- `h0` is about `log (a • h x + b • h y)`; rewrite that argument via `hh`.
 161    simpa [Function.comp, smul_eq_mul, hh] using h0
 162
 163  -- scale by positive constant: gapR = (1/log φ) * (log ∘ h)
 164  refine ⟨h_log_comp.1, ?_⟩
 165  intro x hx y hy hxy a b ha hb hab
 166  have hc : 0 < (1 / Real.log phi) := one_div_pos.2 hlogφpos
 167  have hbase := h_log_comp.2 hx hy hxy ha hb hab
 168  -- rewrite `gapR` as a constant multiple of `log (h x)`
 169  have hdef : ∀ t : ℝ, gapR t = (1 / Real.log phi) * g (h t) := by
 170    intro t
 171    simp [gapR, g, h, div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm]
 172  -- multiply strict inequality by positive constant and distribute
 173  have hmul : (1 / Real.log phi) * (a * (g (h x)) + b * (g (h y))) <
 174      (1 / Real.log phi) * (g (h (a • x + b • y))) := by
 175    -- `smul` on ℝ is multiplication; `hbase` is already in that form
 176    have := mul_lt_mul_of_pos_left hbase hc
 177    -- rewrite scalar multiplications
 178    simpa [smul_eq_mul, mul_add, add_mul, mul_assoc, mul_left_comm, mul_comm] using this
 179  -- convert back to gapR and finish
 180  -- LHS: a*gapR x + b*gapR y  ; RHS: gapR(a•x + b•y)
 181  have : a * gapR x + b * gapR y < gapR (a • x + b • y) := by
 182    -- rewrite all gapR occurrences using hdef, then use hmul
 183    simpa [hdef, smul_eq_mul, mul_add, add_mul, mul_assoc, mul_left_comm, mul_comm] using hmul
 184  simpa [StrictConcaveOn, smul_eq_mul] using this
 185
 186/-!
 187Diminishing increments: for `n ≥ 0`, the discrete first differences decrease.
 188
 189This is the discrete shadow of strict concavity:
 190\[
 191-- ... 4 more lines elided ...