theorem
proved
tactic proof
rigid_rotation_energy_lower_bound
show as:
view Lean formalization →
formal statement (Lean)
190private theorem rigid_rotation_energy_lower_bound {ω₀ R : ℝ} (hω₀ : ω₀ ≠ 0) (hR : 0 < R) :
191 ((ω₀ / 2) ^ 2) * R ^ 4 / 64 ≤
192 ∫ x in Metric.ball (0 : ℝ × ℝ) R, ((ω₀ / 2) ^ 2) * (x.1 ^ 2 + x.2 ^ 2) := by
proof body
Tactic-mode proof.
193 let c : ℝ := (ω₀ / 2) ^ 2
194 let rect : Set (ℝ × ℝ) := Set.Icc (R / 2) (3 * R / 4) ×ˢ Set.Icc 0 (R / 4)
195 let f : ℝ × ℝ → ℝ := fun x => c * (x.1 ^ 2 + x.2 ^ 2)
196 have hc_nonneg : 0 ≤ c := by
197 dsimp [c]
198 positivity
199 have hrect_subset_ball : rect ⊆ Metric.ball (0 : ℝ × ℝ) R := by
200 intro x hx
201 rcases hx with ⟨hx1, hx2⟩
202 rw [Metric.mem_ball, Prod.dist_eq, Real.dist_eq, Real.dist_eq, max_lt_iff]
203 constructor
204 · have hx1_nonneg : 0 ≤ x.1 := by
205 linarith [hx1.1, hR]
206 have hx1_lt : x.1 < R := by
207 linarith [hx1.2, hR]
208 simpa [abs_of_nonneg hx1_nonneg] using hx1_lt
209 · have hx2_nonneg : 0 ≤ x.2 := hx2.1
210 have hx2_lt : x.2 < R := by
211 linarith [hx2.2, hR]
212 simpa [abs_of_nonneg hx2_nonneg] using hx2_lt
213 have hf_cont : Continuous f := by
214 dsimp [f]
215 continuity
216 have hf_int_closed : IntegrableOn f (Metric.closedBall (0 : ℝ × ℝ) R) volume := by
217 exact hf_cont.continuousOn.integrableOn_compact
218 (isCompact_closedBall (x := (0 : ℝ × ℝ)) (r := R))
219 have hf_int_ball : IntegrableOn f (Metric.ball (0 : ℝ × ℝ) R) volume :=
220 hf_int_closed.mono_set Metric.ball_subset_closedBall
221 have hf_nonneg_ball : 0 ≤ᵐ[volume.restrict (Metric.ball (0 : ℝ × ℝ) R)] f := by
222 refine MeasureTheory.ae_restrict_of_forall_mem (Metric.isOpen_ball.measurableSet) ?_
223 intro x hx
224 dsimp [f]
225 positivity
226 have hball_ge_rect :
227 ∫ x in rect, f x ∂volume ≤ ∫ x in Metric.ball (0 : ℝ × ℝ) R, f x ∂volume := by
228 refine MeasureTheory.setIntegral_mono_set hf_int_ball hf_nonneg_ball ?_
229 exact Filter.Eventually.of_forall hrect_subset_ball
230 have hf_int_rect : IntegrableOn f rect volume := hf_int_ball.mono_set hrect_subset_ball
231 have hrect_compact : IsCompact rect := by
232 exact isCompact_Icc.prod isCompact_Icc
233 have hconst_int : IntegrableOn (fun _ : ℝ × ℝ => c * (R / 2) ^ 2) rect volume := by
234 simpa using
235 (MeasureTheory.integrableOn_const (μ := (volume : MeasureTheory.Measure (ℝ × ℝ)))
236 (s := rect) (C := c * (R / 2) ^ 2) (hs := hrect_compact.measure_lt_top.ne))
237 have hconst_le : (fun _ : ℝ × ℝ => c * (R / 2) ^ 2) ≤ᵐ[volume.restrict rect] f := by
238 refine MeasureTheory.ae_restrict_of_forall_mem ?_ ?_
239 · exact measurableSet_Icc.prod measurableSet_Icc
240 · intro x hx
241 rcases hx with ⟨hx1, hx2⟩
242 have hR2 : 0 ≤ R / 2 := by
243 linarith
244 have hx10 : 0 ≤ x.1 := le_trans hR2 hx1.1
245 have hx1sq : (R / 2) ^ 2 ≤ x.1 ^ 2 := by
246 exact (sq_le_sq₀ (a := R / 2) (b := x.1) hR2 hx10).2 hx1.1
247 dsimp [f]
248 nlinarith [hc_nonneg, hx1sq, sq_nonneg x.2]
249 have hrect_lower :
250 ∫ x in rect, c * (R / 2) ^ 2 ∂volume ≤ ∫ x in rect, f x ∂volume :=
251 MeasureTheory.setIntegral_mono_ae_restrict hconst_int hf_int_rect hconst_le
252 have hrect_measure : (volume : MeasureTheory.Measure (ℝ × ℝ)).real rect = (R / 4) * (R / 4) := by
253 let sx : Set ℝ := Set.Icc (R / 2) (3 * R / 4)
254 let sy : Set ℝ := Set.Icc 0 (R / 4)
255 have hprod :
256 (MeasureTheory.volume : MeasureTheory.Measure (ℝ × ℝ)) (sx ×ˢ sy) =
257 (MeasureTheory.volume : MeasureTheory.Measure ℝ) sx *
258 (MeasureTheory.volume : MeasureTheory.Measure ℝ) sy :=
259 MeasureTheory.Measure.prod_prod _ _
260 have hx : 3 * R / 4 - R / 2 = R / 4 := by
261 ring
262 change ENNReal.toReal ((MeasureTheory.volume : MeasureTheory.Measure (ℝ × ℝ)) (sx ×ˢ sy)) =
263 (R / 4) * (R / 4)
264 rw [hprod]
265 simp [sx, sy, Real.volume_Icc, hx, show 0 ≤ R / 4 by linarith]
266 have hconst_eval :
267 ∫ x in rect, c * (R / 2) ^ 2 ∂volume = (R / 4) * (R / 4) * (c * (R / 2) ^ 2) := by
268 calc
269 ∫ x in rect, c * (R / 2) ^ 2 ∂volume =
270 (volume : MeasureTheory.Measure (ℝ × ℝ)).real rect * (c * (R / 2) ^ 2) := by
271 simp [MeasureTheory.integral_const]
272 _ = (R / 4) * (R / 4) * (c * (R / 2) ^ 2) := by
273-- ... 15 more lines elided ...