Prove2Me

Continuity of the Generator for C3C^3 Functions

Proved
FunctionalInequalities.KLS.BKL.Localization.continuous_generator_of_contDiff_three_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement shows that the localization generator is continuous on every C3C^3 test function.

Let μ\mu be a compactly supported isotropic probability law on EuclideanSpace⁡(R,Fin⁡n)\operatorname{EuclideanSpace}(\mathbb{R},\operatorname{Fin}n). If FF on the localization parameter space satisfies

F∈C3,F\in C^3,

then the function q↦generator⁡(μ,hc,F)(q)q\mapsto\operatorname{generator}(\mu,h_c,F)(q) is continuous:

Continuous⁡(generator⁡(μ,hc,F)).\operatorname{Continuous}(\operatorname{generator}(\mu,h_c,F)).

The result is a regularity lemma for subsequent generator integration and comparison arguments.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.BKL.Localization. Shown in its original module context. Proof omitted.

theorem continuous_generator_of_contDiff_three (hiso : KLS.Isotropic μ) {F : Param n → ℝ}
    (hF : ContDiff ℝ 3 F) : Continuous (generator μ hc F)

Module navigation

Module: KLS/BKL/Localization/Energy/Regularity.

Definition modules: KLS/BKL/Localization/Coefficients, KLS/Isotropic.

Supporting theorems: Covariance.inner_operator_self_pos_of_affineSupport_eq_top, locallyLipschitz_noise, Isotropic.locallyLipschitz_inverseSqrt_covariance_joint, contDiff_posteriorCovariance_joint, contDiff_posteriorMean_joint.

Previous: contDiff_cumulantEnergy_posterior.

Source excerpt, lines 91–92 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_Energy_Regularity

variable {n : ℕ} (μ : MeasureTheory.ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
  (hc : IsCompact (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))).support)
Formal statement

theorem FunctionalInequalities.KLS.BKL.Localization.continuous_generator_of_contDiff_three_readable (hiso : KLS.Isotropic μ) {F : Param n → ℝ}
    (hF : ContDiff ℝ 3 F) : Continuous (generator μ hc F) := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/Localization/Energy/Regularity.lean#L90-L125 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Localization.Energy.Regularity`, declaration `FunctionalInequalities.KLS.BKL.Localization.continuous_generator_of_contDiff_three`; the repository is private at upload time).

View graph