Statement solution surface

The statement-level definitions are repeated under QuadraticCarleson.StatementSurface so Comparator can compare this module independently with Challenge.lean. Each theorem is then obtained by definitional transport from the canonical theorem in QuadraticCarleson.PaperTheorems.

noncomputable def QuadraticCarleson.StatementSurface.phase (s : ℝ) : ℂ

The unit complex phase with exponent 2πis used in the statement surface.

Equations

• QuadraticCarleson.StatementSurface.phase s = Complex.exp (↑(2 * Real.pi * s) * Complex.I)

noncomputable def QuadraticCarleson.StatementSurface.paperLog : ℕ → ℝ → ℝ

The iterated logarithm with additive shift ten at each iteration.

Equations

• QuadraticCarleson.StatementSurface.paperLog 0 = id
• QuadraticCarleson.StatementSurface.paperLog n.succ = fun (t : ℝ) => Real.log (10 + QuadraticCarleson.StatementSurface.paperLog n t)

def QuadraticCarleson.StatementSurface.GrowsSlowerThanEndpoint (Phi : YoungFunction) : Prop

Little-o growth relative to the endpoint function t * paperLog 2 t at infinity.

Equations

• QuadraticCarleson.StatementSurface.GrowsSlowerThanEndpoint Phi = (fun (t : ℝ) => Phi.toFun t) =o[Filter.atTop] fun (t : ℝ) => t * QuadraticCarleson.StatementSurface.paperLog 2 t

noncomputable def QuadraticCarleson.StatementSurface.quadraticHilbertTrunc (modulation epsilon : ℝ) (f : ℝ → ℂ) (x : ℝ) : ℂ

The quadratic Hilbert integral truncated outside the symmetric interval of radius epsilon.

Equations

• One or more equations did not get rendered due to their size.

def QuadraticCarleson.StatementSurface.HasQuadraticPrincipalValue (modulation : ℝ) (f : ℝ → ℂ) (x : ℝ) (z : ℂ) : Prop

Convergence of the truncated quadratic Hilbert integrals as the positive cutoff tends to zero.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuadraticCarleson.StatementSurface.dyadicModulation (n : ℤ) : ℝ

The dyadic modulation corresponding to an integer exponent.

Equations

• QuadraticCarleson.StatementSurface.dyadicModulation n = 2 ^ n

noncomputable def QuadraticCarleson.StatementSurface.principalValueRepresentative (lam : ℝ) (f : L0Infinity) (x : ℝ) : ℂ

The chosen quadratic principal value when it exists, and zero otherwise.

Equations

• QuadraticCarleson.StatementSurface.principalValueRepresentative lam f x = if h : ∃ (z : ℂ), QuadraticCarleson.StatementSurface.HasQuadraticPrincipalValue lam f.toFun x z then h.choose else 0

noncomputable def QuadraticCarleson.StatementSurface.fullPrincipalValueMaximal (f : L0Infinity) (x : ℝ) : ENNReal

The supremum of principal-value norms over all real modulations.

Equations

• QuadraticCarleson.StatementSurface.fullPrincipalValueMaximal f x = ⨆ (lam : ℝ), ENNReal.ofReal ‖QuadraticCarleson.StatementSurface.principalValueRepresentative lam f x‖

noncomputable def QuadraticCarleson.StatementSurface.lacunaryPrincipalValueMaximal (f : L0Infinity) (x : ℝ) : ENNReal

The supremum of principal-value norms over the dyadic modulation sequence.

Equations

• One or more equations did not get rendered due to their size.

def QuadraticCarleson.StatementSurface.functionOperatorLevelSet (T : L0Infinity → ℝ → ENNReal) (f : L0Infinity) (alpha : ℝ) : Set ℝ

The set where the operator on a test function exceeds the specified real level.

Equations

• QuadraticCarleson.StatementSurface.functionOperatorLevelSet T f alpha = {x : ℝ | ENNReal.ofReal alpha < T f x}

def QuadraticCarleson.StatementSurface.HasFunctionPhiModularEstimate (Phi : YoungFunction) (T : L0Infinity → ℝ → ENNReal) : Prop

A uniform distributional estimate by the Young-function modular of each normalized test input.

Equations

• One or more equations did not get rendered due to their size.

theorem QuadraticCarleson.StatementSurface.PaperTheorems.lacunary_sub_log2_modular_failure (Phi : YoungFunction) (hPhi : GrowsSlowerThanEndpoint Phi) : ¬HasFunctionPhiModularEstimate Phi lacunaryPrincipalValueMaximal

theorem QuadraticCarleson.StatementSurface.PaperTheorems.full_sub_log2_modular_failure (Phi : YoungFunction) (hPhi : GrowsSlowerThanEndpoint Phi) : ¬HasFunctionPhiModularEstimate Phi fullPrincipalValueMaximal

theorem QuadraticCarleson.StatementSurface.PaperTheorems.full_LlogL_endpoint : ∃ K < ⊤, ∀ (f : L0Infinity), (∀ᵐ (x : ℝ), ∀ (lam : ℝ), HasQuadraticPrincipalValue lam f.toFun x (principalValueRepresentative lam f x)) ∧ ∀ (α : ℝ), 0 < α → MeasureTheory.volume {x : ℝ | ENNReal.ofReal α < fullPrincipalValueMaximal f x} ≤ K * ∫⁻ (x : ℝ), ENNReal.ofReal (‖f.toFun x‖ / α * paperLog 1 (‖f.toFun x‖ / α))

theorem QuadraticCarleson.StatementSurface.PaperTheorems.lacunary_log2_squared_log4_endpoint : ∃ K < ⊤, ∀ (f : L0Infinity), (∀ᵐ (x : ℝ), ∀ (m : ℤ), HasQuadraticPrincipalValue (dyadicModulation m) f.toFun x (principalValueRepresentative (dyadicModulation m) f x)) ∧ ∀ (α : ℝ), 0 < α → MeasureTheory.volume {x : ℝ | ENNReal.ofReal α < lacunaryPrincipalValueMaximal f x} ≤ K * ∫⁻ (x : ℝ), ENNReal.ofReal (‖f.toFun x‖ / α * paperLog 2 (‖f.toFun x‖ / α) ^ 2 * paperLog 4 (‖f.toFun x‖ / α))