Critical logarithmic weight on the four-torus

The binary convolution of two inverse-square kernels has a logarithmic singularity. This file packages the elementary pointwise inequalities needed to average that logarithm at a moving mollifier scale.

noncomputable def Anderson4D.criticalLogWeight (z : T4) : ℝ

The nonnegative critical weight produced by the sharp binary inverse-square convolution. Mathlib uses Real.log 0 = 0; this harmless value agrees with all a.e. applications below.

Equations

• Anderson4D.criticalLogWeight z = 1 + |Real.log ‖z‖|

theorem Anderson4D.criticalLogWeight_nonneg (z : T4) : 0 ≤ criticalLogWeight z

theorem Anderson4D.measurable_criticalLogWeight : Measurable criticalLogWeight

noncomputable def Anderson4D.invSqKerHalf (z : T4) : ℝ

The half-power kernel |z|⁻¹, expressed intrinsically through the paper's inverse-square model.

Equations

• Anderson4D.invSqKerHalf z = Anderson4D.invSqKer z ^ (1 / 2)

theorem Anderson4D.invSqKerHalf_nonneg (z : T4) : 0 ≤ invSqKerHalf z

theorem Anderson4D.measurable_invSqKerHalf : Measurable invSqKerHalf

theorem Anderson4D.one_add_abs_log_le_scaled_inv {r t A : ℝ} (hr : 0 < r) (ht : 0 < t) (htA : t ≤ A * r) : 1 + |Real.log t| ≤ 1 + |Real.log r| + A + r / t

Scale-relative logarithmic inequality. The only singular term is r / t; all remaining losses are an absolute constant, the fixed aperture A, and |log r|.

theorem Anderson4D.inv_norm_le_two_mul_invSqKerHalf {z : T4} (hz : z ≠ 0) : ‖z‖⁻¹ ≤ 2 * invSqKerHalf z

The inverse norm is controlled by twice the intrinsic half-power kernel. The factor two is exactly the comparison torusDistSq z ≤ 4 ‖z‖².

theorem Anderson4D.invSqKer_mul_half_le_threeHalf_add (u v : T4) : invSqKer u * invSqKerHalf v ≤ invSqKerThreeHalf u + invSqKerThreeHalf v

Weighted Young inequality at the exponents used in the local logarithmic convolution.

theorem Anderson4D.criticalLogWeight_le_scaled_half {r A : ℝ} (hr : 0 < r) (hA : 0 ≤ A) (z : T4) (hz : ‖z‖ ≤ A * r) : criticalLogWeight z ≤ 1 + |Real.log r| + A + 2 * r * invSqKerHalf z

Near one fixed scale, the critical logarithm is a constant scale-log plus a single half-power singularity.

theorem Anderson4D.inv_norm_sq_le_four_mul_invSqKer {z : T4} (hz : z ≠ 0) : ‖z‖⁻¹ ^ 2 ≤ 4 * invSqKer z

Squared inverse-norm comparison, used when a bounded density rather than an inverse-square factor is averaged against the logarithm.

theorem Anderson4D.criticalLogWeight_le_scaled_invSq {r A : ℝ} (hr : 0 < r) (hA : 0 ≤ A) (z : T4) (hz : ‖z‖ ≤ A * r) : criticalLogWeight z ≤ 2 + |Real.log r| + A + 4 * r ^ 2 * invSqKer z

A less singular scale-relative logarithmic inequality, suited to a bounded density on a scale ball.

theorem Anderson4D.norm_t4_le_pi (z : T4) : ‖z‖ ≤ Real.pi

The product torus has diameter at most π in its sup norm.

theorem Anderson4D.criticalLogWeight_le_of_fixedScale {a ε : ℝ} (ha : 0 < a) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (z : T4) (hz : a * ε ≤ ‖z‖) : criticalLogWeight z ≤ (5 + |Real.log a|) * |Real.log ε|

If a torus point stays at least a fixed multiple of ε away from the logarithmic singularity, its critical weight costs only one copy of |log ε|. The constant depends explicitly on that fixed multiple.

theorem Anderson4D.exists_setIntegral_criticalLogWeight_ball_le : ∃ (K : ℝ), 0 < K ∧ ∀ (x : T4) (r : ℝ), 0 < r → ∫ (z : T4) in Metric.ball x r, criticalLogWeight (x - z) ∂paperMeasure ≤ K * r ^ 4 * (3 + |Real.log r|)

The critical logarithm has the expected r⁴(1+|log r|) mass on a four-dimensional torus ball, uniformly in its centre.