 103noncomputable def gapR (x : ℝ) : ℝ :=
 104  Real.log (1 + x / phi) / Real.log phi
 105
 106@[simp] theorem gapR_nat (n : ℕ) : gapR (n : ℝ) = gap (n : ℤ) := by
 107  simp [gapR, gap]
 108
 109/-- `gapR` is strictly concave on `[0,∞)`. -/
 110theorem strictConcaveOn_gapR_Ici : StrictConcaveOn ℝ (Set.Ici (0 : ℝ)) gapR := by
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.