rigid_rotation_energy_lower_bound

formal source

 187  ¬ ∃ E : ℝ, ∀ R > 0, ∫ x in Metric.ball (0 : ℝ × ℝ) R,
 188    (ω₀ / 2)^2 * (x.1^2 + x.2^2) ≤ E
 189
 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
 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