RotationalAveraging

Auxiliary lemmas for the arc bound

Private Lemma 2.6a: Pointwise bound on an arc

For r ≥ 0 and θ ∈ ℝ with |θ| ≤ π/4: rho(r * exp(i θ)) ≥ r / √2

Proof of 2.6a:

• cos(θ) ≥ 1/√2 for |θ| ≤ π/4.
• |1 + r exp(iθ)|² = 1 + 2r cos(θ) + r², so |1 + r exp(iθ)| − 1 = (r² + 2r cos(θ)) / (|1+r exp(iθ)| + 1).
• Numerator ≥ r² + √2 r > 0, so |1+r exp(iθ)| > 1 and rho = |1+…| − 1.
• Denominator ≤ (1 + r) + 1 = r + 2.
• So rho ≥ r(r + √2)/(r + 2) ≥ r/√2.
• Last step: (r + √2)/(r + 2) ≥ 1/√2 <=> (√2 − 1)r ≥ 0. ✓

Auxiliary lemmas for the integral bound

Theorem 2.6: Rotational averaging bound

For r ≥ 0: ∫ t, rho(r * exp(i t))² d(haar) ≥ r² / 8

where the integral is w.r.t. normalized Haar measure on AddCircle T.

Proof: Step 1: On the arc {|θ| ≤ π/4}, rho(r exp(iθ)) ≥ r/√2 (Private Lemma 2.6a). Step 2: The arc has measure 1/4 under Haar. Step 3: ∫ rho² d(haar) ≥ (1/4)(r/√2)² = r²/8.

Lean proof: Convert to an interval integral on ℝ via integral_haarAddCircle and integral_preimage, then bound from below on [-π/4, π/4].

theorem FockSPR.rotational_averaging_bound {r : ℝ} (hr : 0 ≤ r) : ∫ (t : AddCircle T), rho (↑r * (fourier 1) t) ^ 2 ∂AddCircle.haarAddCircle ≥ r ^ 2 / 8