theorem
proved
tactic proof
actionJ_convex_on_interp
show as:
view Lean formalization →
formal statement (Lean)
74theorem actionJ_convex_on_interp (hab : a ≤ b)
75 (γ₁ γ₂ : AdmissiblePath a b) (s : ℝ) (hs : s ∈ Icc (0:ℝ) 1) :
76 actionJ (interp γ₁ γ₂ s hs) ≤ (1 - s) * actionJ γ₁ + s * actionJ γ₂ := by
proof body
Tactic-mode proof.
77 -- Step 1: the integrand is bounded pointwise.
78 have h_pointwise : ∀ t ∈ Set.uIcc a b,
79 Jcost ((interp γ₁ γ₂ s hs).toFun t) ≤
80 (1 - s) * Jcost (γ₁.toFun t) + s * Jcost (γ₂.toFun t) := by
81 intro t ht
82 -- On `[a,b]` (uIcc reduces to Icc since hab), positivity holds.
83 have htIcc : t ∈ Icc a b := by
84 have : Set.uIcc a b = Icc a b := by
85 rw [Set.uIcc_of_le hab]
86 rwa [this] at ht
87 have hp1 : 0 < γ₁.toFun t := γ₁.pos t htIcc
88 have hp2 : 0 < γ₂.toFun t := γ₂.pos t htIcc
89 rw [interp_apply]
90 exact Jcost_convex_combination s hs hp1 hp2
91 -- Step 2: continuity / integrability of all three integrands on [a,b].
92 have h_cont_interp : ContinuousOn (fun t => Jcost ((interp γ₁ γ₂ s hs).toFun t)) (Icc a b) := by
93 have hpos : ∀ t ∈ Icc a b, 0 < (interp γ₁ γ₂ s hs).toFun t :=
94 (interp γ₁ γ₂ s hs).pos
95 -- Jcost is continuous on (0, ∞); composed with the continuous, positive interp.
96 have hJcont : ContinuousOn Jcost (Set.Ioi (0:ℝ)) := by
97 unfold Jcost
98 apply ContinuousOn.sub
99 · apply ContinuousOn.div_const
100 apply ContinuousOn.add continuousOn_id
101 exact continuousOn_inv₀.mono (fun x hx => ne_of_gt hx)
102 · exact continuousOn_const
103 refine ContinuousOn.comp hJcont (interp γ₁ γ₂ s hs).cont ?_
104 intro t htmem
105 exact hpos t htmem
106 have h_cont_1 : ContinuousOn (fun t => Jcost (γ₁.toFun t)) (Icc a b) := by
107 have hJcont : ContinuousOn Jcost (Set.Ioi (0:ℝ)) := by
108 unfold Jcost
109 apply ContinuousOn.sub
110 · apply ContinuousOn.div_const
111 apply ContinuousOn.add continuousOn_id
112 exact continuousOn_inv₀.mono (fun x hx => ne_of_gt hx)
113 · exact continuousOn_const
114 refine ContinuousOn.comp hJcont γ₁.cont ?_
115 intro t htmem; exact γ₁.pos t htmem
116 have h_cont_2 : ContinuousOn (fun t => Jcost (γ₂.toFun t)) (Icc a b) := by
117 have hJcont : ContinuousOn Jcost (Set.Ioi (0:ℝ)) := by
118 unfold Jcost
119 apply ContinuousOn.sub
120 · apply ContinuousOn.div_const
121 apply ContinuousOn.add continuousOn_id
122 exact continuousOn_inv₀.mono (fun x hx => ne_of_gt hx)
123 · exact continuousOn_const
124 refine ContinuousOn.comp hJcont γ₂.cont ?_
125 intro t htmem; exact γ₂.pos t htmem
126 -- Step 3: integrate the pointwise inequality.
127 have h_int_interp : IntervalIntegrable
128 (fun t => Jcost ((interp γ₁ γ₂ s hs).toFun t))
129 MeasureTheory.volume a b :=
130 h_cont_interp.intervalIntegrable_of_Icc hab
131 have h_int_1 : IntervalIntegrable (fun t => Jcost (γ₁.toFun t))
132 MeasureTheory.volume a b :=
133 h_cont_1.intervalIntegrable_of_Icc hab
134 have h_int_2 : IntervalIntegrable (fun t => Jcost (γ₂.toFun t))
135 MeasureTheory.volume a b :=
136 h_cont_2.intervalIntegrable_of_Icc hab
137 -- Form the dominating integrand (1-s) Jcost(γ₁) + s Jcost(γ₂).
138 set rhs : ℝ → ℝ := fun t => (1 - s) * Jcost (γ₁.toFun t) + s * Jcost (γ₂.toFun t)
139 have h_int_rhs : IntervalIntegrable rhs MeasureTheory.volume a b := by
140 refine IntervalIntegrable.add ?_ ?_
141 · exact h_int_1.const_mul (1 - s)
142 · exact h_int_2.const_mul s
143 -- Apply integral monotonicity on [a, b].
144 have h_mono : ∫ t in a..b, Jcost ((interp γ₁ γ₂ s hs).toFun t)
145 ≤ ∫ t in a..b, rhs t := by
146 refine intervalIntegral.integral_mono_on hab h_int_interp h_int_rhs ?_
147 intro t ht
148 have htIcc : t ∈ Icc a b := ht
149 have htUI : t ∈ Set.uIcc a b := by
150 rw [Set.uIcc_of_le hab]; exact htIcc
151 exact h_pointwise t htUI
152 -- Compute the RHS integral.
153 have h_rhs_eq : ∫ t in a..b, rhs t =
154 (1 - s) * (∫ t in a..b, Jcost (γ₁.toFun t)) +
155 s * (∫ t in a..b, Jcost (γ₂.toFun t)) := by
156 show ∫ t in a..b, ((1 - s) * Jcost (γ₁.toFun t) + s * Jcost (γ₂.toFun t)) =
157-- ... 32 more lines elided ...