lemma
proved
tactic proof
Jcost_convex_combination
show as:
view Lean formalization →
formal statement (Lean)
51lemma Jcost_convex_combination (s : ℝ) (hs : s ∈ Icc (0:ℝ) 1)
52 {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
53 Jcost ((1 - s) * x + s * y) ≤ (1 - s) * Jcost x + s * Jcost y := by
proof body
Tactic-mode proof.
54 -- Use ConvexOn version derived from StrictConvexOn.
55 have hconv : ConvexOn ℝ (Ioi (0:ℝ)) Jcost := Jcost_strictConvexOn_pos.convexOn
56 have h1 : (1 - s) + s = 1 := by ring
57 have h0_le : 0 ≤ 1 - s := by linarith [hs.2]
58 have hs_nn : 0 ≤ s := hs.1
59 have hxmem : x ∈ Ioi (0:ℝ) := hx
60 have hymem : y ∈ Ioi (0:ℝ) := hy
61 have := hconv.2 hxmem hymem h0_le hs_nn h1
62 -- The mathlib statement uses `•` (smul). Translate to `*`.
63 simpa [smul_eq_mul] using this
64
65/-! ## Convexity of the action functional -/
66
67/-- **Convexity of the J-action.** For any two admissible paths sharing
68 a domain, the action of the convex interpolation is bounded by the
69 convex combination of the actions.
70
71 `S[(1-s)γ₁ + s γ₂] ≤ (1-s) S[γ₁] + s S[γ₂]`
72
73 This is the integrated form of pointwise convexity of `Jcost`. -/