Logarithmic asymptotics at the positive side of zero

Small filter lemmas for the critical coupling λ_ε = λ / sqrt |log ε|.

theorem Anderson4D.tendsto_abs_log_nhdsGT_zero_atTop : Filter.Tendsto (fun (ε : ℝ) => |Real.log ε|) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop

The absolute logarithm diverges along ε ↓ 0.

theorem Anderson4D.tendsto_truncOrder_nhdsGT_zero_atTop : Filter.Tendsto truncOrder (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop

The paper's integer truncation order tends to infinity as ε ↓ 0.

theorem Anderson4D.eventually_le_truncOrder (B : ℕ) : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), B ≤ truncOrder ε

Every fixed perturbative order is eventually below the moving paper cutoff A = ⌊|log ε|⌋.

theorem Anderson4D.tendsto_inv_abs_log_nhdsGT_zero : Filter.Tendsto (fun (ε : ℝ) => 1 / |Real.log ε|) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

One inverse logarithm vanishes along ε ↓ 0.

theorem Anderson4D.tendsto_const_div_abs_log_nhdsGT_zero (C : ℝ) : Filter.Tendsto (fun (ε : ℝ) => C / |Real.log ε|) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

A fixed constant divided by the absolute logarithm also vanishes.

theorem Anderson4D.eventually_abs_log_pos : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), 0 < |Real.log ε|

The absolute logarithm is eventually strictly positive.

theorem Anderson4D.eventually_smallScale_le {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ε ≤ δ

Every fixed positive upper cutoff is eventually respected as ε ↓ 0.

theorem Anderson4D.eventually_one_le_abs_log : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), 1 ≤ |Real.log ε|

The logarithmic lower bound used in the deterministic estimates is automatic at sufficiently small positive scale.

theorem Anderson4D.eventually_lamEps_pos {lam : ℝ} (hlam : 0 < lam) : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), 0 < lamEps lam ε

A positive critical coupling is eventually positive.

theorem Anderson4D.eventually_lamEps_ne_zero {lam : ℝ} (hlam : 0 < lam) : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), lamEps lam ε ≠ 0

In particular the critical coupling is eventually nonzero.

theorem Anderson4D.eventually_nhdsGT_zero_to_Ioo {P : ℝ → Prop} (hP : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), P ε) : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioo 0 1), P ε

Restricting from the positive punctured side to (0,1) preserves every eventual statement.