English
For θ ∈ ℝ and (x,y) ∈ E×E, rotation θ maps to the pair consisting of cos θ x + sin θ y and -sin θ x + cos θ y.
Русский
Для θ ∈ ℝ и пары (x, y) ∈ E×E поворотом по θ является пара (cos θ x + sin θ y, -sin θ x + cos θ y).
LaTeX
$$$ \mathrm{rotation}(\theta)(x,y) = (\cos \theta \cdot x + \sin \theta \cdot y,
-\sin \theta \cdot x + \cos \theta \cdot y). $$$
Lean4
/-- If a measure `μ` is such that `μ.prod μ` is invariant by rotation of angle `-π/4` then
`μ {x | ‖x‖ ≤ a} * μ {x | b < ‖x‖} ≤ μ {x | (b - a) / √2 < ‖x‖} ^ 2`. -/
theorem measure_le_mul_measure_gt_le_of_map_rotation_eq_self [SFinite μ]
(h : (μ.prod μ).map (ContinuousLinearMap.rotation (-(π / 4))) = μ.prod μ) (a b : ℝ) :
μ {x | ‖x‖ ≤ a} * μ {x | b < ‖x‖} ≤ μ {x | (b - a) / √2 < ‖x‖} ^ 2 := by
calc
μ {x | ‖x‖ ≤ a} * μ {x | b < ‖x‖}
_ = (μ.prod μ) ({x | ‖x‖ ≤ a} ×ˢ {y | b < ‖y‖}) := by
rw [Measure.prod_prod]
-- This is the measure of two bands in the plane (draw a picture!)
_ = (μ.prod μ) {p | ‖p.1‖ ≤ a ∧ b < ‖p.2‖} := rfl
_ = ((μ.prod μ).map (ContinuousLinearMap.rotation (-(π / 4)))) {p | ‖p.1‖ ≤ a ∧ b < ‖p.2‖} := by
-- We can rotate the bands since `μ.prod μ` is invariant under rotation
rw [h]
_ = (μ.prod μ) {p | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2} :=
by
rw [Measure.map_apply (by fun_prop)]
swap
· refine MeasurableSet.inter ?_ ?_
· change MeasurableSet {p : E × E | ‖p.1‖ ≤ a}
exact measurableSet_le (by fun_prop) (by fun_prop)
· change MeasurableSet {p : E × E | b < ‖p.2‖}
exact measurableSet_lt (by fun_prop) (by fun_prop)
congr 1
simp only [Set.preimage_setOf_eq, ContinuousLinearMap.rotation_apply, Real.cos_neg, Real.cos_pi_div_four,
Real.sin_neg, Real.sin_pi_div_four, neg_smul, neg_neg]
have h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹ :=
by
simp only [norm_mul, norm_inv, Real.norm_ofNat, Real.norm_eq_abs]
rw [abs_of_nonneg (by positivity)]
nth_rw 1 [← Real.sq_sqrt (by simp : (0 : ℝ) ≤ 2)]
rw [pow_two, mul_inv, mul_assoc, inv_mul_cancel₀ (by positivity), mul_one]
congr! with p
· rw [← sub_eq_add_neg, ← smul_sub, norm_smul, div_eq_inv_mul, div_eq_inv_mul]
congr
· rw [← smul_add, norm_smul, div_eq_inv_mul, div_eq_inv_mul]
congr
_ ≤ (μ.prod μ) {p | (b - a) / √2 < ‖p.1‖ ∧ (b - a) / √2 < ‖p.2‖} := by
-- The rotated bands are contained in quadrants.
refine measure_mono fun p ↦ ?_
simp only [Set.mem_setOf_eq, and_imp]
intro hp1 hp2
suffices (b - a) / √2 < min ‖p.1‖ ‖p.2‖ from lt_min_iff.mp this
calc
(b - a) / √2
_ < (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 :=
by
suffices b - a < ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2 by
calc
(b - a) / √2 < (‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2) / √2 := by gcongr
_ = (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 := by field_simp; rw [Real.sq_sqrt (by positivity)]; ring
calc
b - a < ‖p.1 + p.2‖ / √2 - a := by gcongr
_ ≤ ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2 := by gcongr
_ ≤ min ‖p.1‖ ‖p.2‖ := by
have := norm_add_sub_norm_sub_le_two_mul_min p.1 p.2
linarith
_ = (μ.prod μ) ({x | (b - a) / √2 < ‖x‖} ×ˢ {y | (b - a) / √2 < ‖y‖}) := rfl
_ ≤ μ {x | (b - a) / √2 < ‖x‖} ^ 2 := by rw [Measure.prod_prod, pow_two]
