PV Infrastructure: Annulus Bounds

Measure-theoretic and analytic bounds on annular regions around crossing points, used in the dyadic PV convergence proof.

Main Results

• annulus_t_measure_bound — t-measure of gamma-annulus
• remainder_integral_bound_on_annulus — remainder integral over annulus is O(epsilon)
• annulus_symmDiff_measure_bound — symmetric difference between gamma-annulus and linear-model annulus
• singular_annulus_bound_explicit — epsilon-independent bound on singular annulus integral

theorem annulus_t_measure_bound {γ : ℝ → ℂ} {a b t₀ : ℝ} {L : ℂ} {ε₁ ε₂ δ₁ : ℝ} (hL : L ≠ 0) (hε₁_pos : 0 < ε₁) (h_lower : ∀ (t : ℝ), 0 < |t - t₀| → |t - t₀| < δ₁ → ‖γ t - γ t₀‖ ≥ ‖L‖ / 2 * |t - t₀|) (h_localize : ∀ t ∈ Set.Icc a b, ‖γ t - γ t₀‖ ≤ ε₁ → |t - t₀| < min δ₁ δ₁) (t : ℝ) (ht_ab : t ∈ Set.Icc a b) (ht_ne : t ≠ t₀) (_hγ_lower : ε₂ < ‖γ t - γ t₀‖) (hγ_upper : ‖γ t - γ t₀‖ ≤ ε₁) : |t - t₀| ≤ 2 * ε₁ / ‖L‖

theorem remainder_integral_bound_on_annulus {γ : ℝ → ℂ} {a b t₀ C δ₀ δ₁ ε₁ ε₂ : ℝ} {L : ℂ} (hL : L ≠ 0) (hε₁_pos : 0 < ε₁) (hε₂_pos : 0 < ε₂) (hr_bounded : ∀ (t : ℝ), 0 < |t - t₀| → |t - t₀| < δ₀ → ‖(γ t - γ t₀)⁻¹ * deriv γ t - (↑(t - t₀))⁻¹‖ ≤ C) (h_lower : ∀ (t : ℝ), 0 < |t - t₀| → |t - t₀| < δ₁ → ‖γ t - γ t₀‖ ≥ ‖L‖ / 2 * |t - t₀|) (h_localize : ∀ t ∈ Set.Icc a b, ‖γ t - γ t₀‖ ≤ ε₁ → |t - t₀| < min δ₀ δ₁) (hat₀ : t₀ ∈ Set.Ioo a b) : have r := fun (t : ℝ) => (γ t - γ t₀)⁻¹ * deriv γ t - (↑(t - t₀))⁻¹; ‖∫ (t : ℝ) in a..b, if ε₂ < ‖γ t - γ t₀‖ ∧ ‖γ t - γ t₀‖ ≤ ε₁ then r t else 0‖ ≤ max 0 C * (4 * ε₁ / ‖L‖)

theorem norm_linear_approx_bound {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} {K₀ δ₀ : ℝ} (h_quad : ∀ (t : ℝ), |t - t₀| < δ₀ → ‖γ t - γ t₀ - (t - t₀) • L‖ ≤ K₀ * |t - t₀| ^ 2) {t : ℝ} (ht : |t - t₀| < δ₀) : |‖γ t - γ t₀‖ - ‖L‖ * |t - t₀|| ≤ K₀ * |t - t₀| ^ 2

theorem volume_shell_le {t₀ r₁ r₂ : ℝ} (hr : r₁ ≤ r₂) : MeasureTheory.volume {t : ℝ | r₁ < |t - t₀| ∧ |t - t₀| ≤ r₂} ≤ ENNReal.ofReal (2 * (r₂ - r₁))

theorem symmDiff_subset_boundaryLayers {g x e ε₁ ε₂ : ℝ} (h_approx : |g - x| ≤ e) (h_xor : Xor (ε₂ < g ∧ g ≤ ε₁) (ε₂ < x ∧ x ≤ ε₁)) : |x - ε₂| ≤ e ∨ |x - ε₁| ≤ e

theorem tAnnLin_implies_r_le {L_norm r ε₁ : ℝ} (hL_pos : 0 < L_norm) (h_in : L_norm * r ≤ ε₁) : r ≤ ε₁ / L_norm

theorem near_threshold_implies_r_in_shell {L_norm r ε K₀ R_max : ℝ} (hL_pos : 0 < L_norm) (hK₀_nonneg : 0 ≤ K₀) (hR_max_nonneg : 0 ≤ R_max) (hr_le : r ≤ R_max) (hr_nonneg : 0 ≤ r) (h_near : |L_norm * r - ε| ≤ K₀ * r ^ 2) : (ε - K₀ * R_max ^ 2) / L_norm ≤ r ∧ r ≤ (ε + K₀ * R_max ^ 2) / L_norm

theorem shell_vol_le {t₀ ε Δ L_norm : ℝ} (hL_pos : 0 < L_norm) (hΔ_nonneg : 0 ≤ Δ) (_hε_pos : 0 < ε) : MeasureTheory.volume {t : ℝ | |L_norm * |t - t₀| - ε| ≤ Δ} ≤ ENNReal.ofReal (4 * Δ / L_norm)

theorem annulus_symmDiff_measure_bound {γ : ℝ → ℂ} {a b t₀ : ℝ} {L : ℂ} (_hab : a < b) (ht₀ : t₀ ∈ Set.Ioo a b) (hγ_C2 : ContDiffAt ℝ 2 γ t₀) (hγ_deriv : deriv γ t₀ = L) (hL : L ≠ 0) : ∃ K > 0, ∃ δ₀' > 0, ∃ δ > 0, ∀ (ε₁ ε₂ : ℝ), 0 < ε₂ → ε₂ ≤ ε₁ → ε₁ < δ → have γAnn := {t : ℝ | t ∈ Set.Icc a b ∧ |t - t₀| < δ₀' ∧ ε₂ < ‖γ t - γ t₀‖ ∧ ‖γ t - γ t₀‖ ≤ ε₁}; have tAnnLin := {t : ℝ | t ∈ Set.Icc a b ∧ |t - t₀| < δ₀' ∧ ε₂ < ‖L‖ * |t - t₀| ∧ ‖L‖ * |t - t₀| ≤ ε₁}; MeasureTheory.volume (symmDiff γAnn tAnnLin) ≤ ENNReal.ofReal (K * ε₁ ^ 2 / ‖L‖ ^ 3)