AutoSamplingTheory.TechnicalLemmas.Registry

No declaration docstring.

inductive LemmaMemoryStatus where
  | formalizedLocal
  | portCandidate
  | sourceGap
  | referenceOnly
deriving Repr, DecidableEq

/-- Metadata for a lemma-memory entry.  The executable proof is the declaration
named in `localDecl`; this structure is only the retrieval record used by
agents and documentation exports. -/

AutoSamplingTheory/TechnicalLemmas/Registry.lean:43published source at 77184245109a

- Metadata for a lemma-memory entry. The executable proof is the declaration named in `localDecl`; this structure is only the retrieval record used by agents and documentation exports.

structure LemmaMemoryEntry where
  key : String
  localDecl : String
  upstreamDecl : String
  upstreamFile : String
  status : LemmaMemoryStatus
  tags : List String
  saldUse : String
  note : String
deriving Repr, DecidableEq

AutoSamplingTheory/TechnicalLemmas/Registry.lean:53published source at 77184245109a

No declaration docstring.

def sltSourceAnchor (file decl note : String) : SourceAnchor :=
  sourceAnchor
    ("slt-" ++ file ++ "-" ++ decl)
    "externalLean"
    "https://github.com/YuanheZ/lean-stat-learning-theory"
    (file ++ ":" ++ decl)
    note

AutoSamplingTheory/TechnicalLemmas/Registry.lean:64published source at 77184245109a

No declaration docstring.

def analysisMemory : List LemmaMemoryEntry := [
  {
    key := "analysis.integrability.of-real-lintegral-finite",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.Integrability.lintegral_ofReal_ne_top_of_integrable_nonneg",
    upstreamDecl := "lintegral_ofReal_ne_top_iff_integrable",
    upstreamFile := "Mathlib.MeasureTheory.Function.L1Space.Integrable",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "integrability", "lintegral", "ENNReal", "ofReal", "nonnegative"],
    saldUse := "Chewi DENS/ANALYSIS root: turn real-valued tail integrability estimates into finite ENNReal density integrals",
    note := "Generic bridge used by Gibbs and future Renyi/Hellinger finite-integral leaves."
  },
  {
    key := "analysis.integrability.gaussian-quadratic-tail",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.Integrability.integrable_exp_neg_mul_norm_sq",
    upstreamDecl := "GaussianFourier.integrable_cexp_neg_mul_sq_norm_add",
    upstreamFile := "Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "integrability", "Lebesgue", "Gaussian-tail", "quadratic", "finite-dimensional"],
    saldUse := "Chewi DENS/CONV root: finite-dimensional Lebesgue integrability of `exp (-a * ‖x‖^2)` for coercive Gibbs envelopes",
    note := "Mathlib-backed high-dimensional Gaussian tail integrability leaf; extracted from the complex Fourier Gaussian API."
  },
  {
    key := "analysis.integrability.shifted-gaussian-quadratic-tail",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.Integrability.integrable_exp_neg_add_mul_norm_sq",
    upstreamDecl := "integrable_exp_neg_mul_norm_sq / Real.exp_add",
    upstreamFile := "AutoSamplingTheory.TechnicalLemmas.Analysis.Integrability",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "integrability", "Lebesgue", "Gaussian-tail", "quadratic", "shifted"],
    saldUse := "Chewi DENS/CONV root: integrability of shifted quadratic envelopes `exp (-(a‖x‖^2+b))`",
    note := "Keeps additive constants in coercive lower potentials separate from the Gaussian tail theorem."
  },
  {
    key := "analysis.integrability.centered-gaussian-quadratic-tail",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.Integrability.integrable_exp_neg_add_mul_norm_sub_sq",
    upstreamDecl := "integrable_exp_neg_add_mul_norm_sq / Integrable.comp_sub_right",
    upstreamFile := "AutoSamplingTheory.TechnicalLemmas.Analysis.Integrability; Mathlib.MeasureTheory.Group.Integral",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "integrability", "Lebesgue", "Gaussian-tail", "quadratic", "centered"],
    saldUse := "Chewi DENS/CONV root: integrability of translated quadratic envelopes `exp (-(a‖x-m‖^2+b))`",
    note := "Fills the center-translation gap for mode-centered strongly convex Gibbs envelopes; does not claim a general coercive-tail theorem."
  },
  {
    key := "analysis.integrability.laplace-absolute-linear-tail",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.Integrability.integrable_exp_neg_add_mul_abs",
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Registry.lean:72published source at 77184245109a

Excerpt truncated; the exact source link is authoritative.

No declaration docstring.

def gaussianMemory : List LemmaMemoryEntry := [
  {
    key := "gaussian.product.coordinate-law",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.ProbabilityDistributions.Gaussian.map_eval_stdGaussianPi",
    upstreamDecl := "map_eval_stdGaussianPi",
    upstreamFile := "SLT/GaussianMeasure.lean",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["gaussian", "coordinate-law", "brownian-increment"],
    saldUse := "normalized scalar coordinate law in the Brownian/Ito EM backend",
    note := "ASTIS-native product-Gaussian coordinate projection theorem."
  },
  {
    key := "gaussian.product.coordinate-integrable",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.ProbabilityDistributions.Gaussian.integrable_eval_stdGaussianPi",
    upstreamDecl := "integrable_eval_stdGaussianPi",
    upstreamFile := "SLT/GaussianMeasure.lean",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["gaussian", "integrability", "coordinate", "brownian-increment"],
    saldUse := "Brownian/Ito coordinate integrability for scalar Taylor moment and generator leaves",
    note := "Cycle 203 lower_3 ASTIS-owned port; uses Mathlib Gaussian exponential integrability and Measure.map transport."
  },
  {
    key := "gaussian.product.coordinate-square-integrable",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.ProbabilityDistributions.Gaussian.integrable_sq_eval_stdGaussianPi",
    upstreamDecl := "integrable_sq_eval_stdGaussianPi",
    upstreamFile := "SLT/GaussianMeasure.lean",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["gaussian", "integrability", "quadratic-moment", "brownian-increment"],
    saldUse := "Brownian/Ito coordinate square integrability for polynomial moment leaves",
    note := "Cycle 203 lower_3 ASTIS-owned port; reuses the local quadratic Gaussian integrability lemma."
  },
  {
    key := "gaussian.product.linear-form-integrable",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.ProbabilityDistributions.Gaussian.integrable_linearForm_stdGaussianPi",
    upstreamDecl := "finite-sum closure of integrable_eval_stdGaussianPi",
    upstreamFile := "Mathlib.MeasureTheory.Function.L1Space.Integrable; ASTIS Gaussian",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["gaussian", "product-gaussian", "linear-form", "integrability", "brownian-increment", "Esscher"],
    saldUse := "finite-dimensional Gaussian linear-function integrability before MGF, Esscher tilt, and Brownian increment packaging",
    note := "Small ASTIS-owned closure lemma; keeps product-Gaussian linear forms separate from exponential tilt/MGF work."
  },
  {
    key := "gaussian.product.coordinate-mean-zero",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.ProbabilityDistributions.Gaussian.integral_eval_stdGaussianPi",
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Registry.lean:295published source at 77184245109a

Excerpt truncated; the exact source link is authoritative.

No declaration docstring.

def taylorMemory : List LemmaMemoryEntry := [
  {
    key := "taylor.hessian.source-field-to-opnorm",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Taylor.hessianOpNormOfSourceHessianField",
    upstreamDecl := "deriv2_bounded_of_compactlySupported",
    upstreamFile := "SLT/GaussianPoincare/TaylorBound.lean",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["taylor", "hessian", "source-contract"],
    saldUse := "convert source-supplied selected-test Hessian representative into downstream Hessian operator-norm bound",
    note := "Does not prove that the SALD source supplies the Hessian field; it only packages the local bridge once supplied."
  },
  {
    key := "taylor.fderiv-hessian-to-iterated",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Taylor.iteratedFDerivTwoOpNormOfFDerivFDerivOpNorm",
    upstreamDecl := "taylor_order_one / TaylorBound proof idiom",
    upstreamFile := "SLT/GaussianPoincare/TaylorBound.lean",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["taylor", "iteratedFDeriv", "hessian"],
    saldUse := "feed selected-line Taylor bounds from a Hessian operator-norm field",
    note := "ASTIS-owned Mathlib bridge."
  },
  {
    key := "brownian.quadratic-variation-normalization",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Taylor.quadraticVariationNormalizationOfCoeffDefAndVarianceOne",
    upstreamDecl := "not upstream; extracted from SALD local proof needs",
    upstreamFile := "ASTIS/SALD cycles 174-176",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["brownian", "ito", "quadratic-variation", "normalization"],
    saldUse := "assemble quadratic coefficient and variance-one fields without re-assuming the downstream normalization",
    note := "Pure algebraic bridge made reusable for later SDE papers."
  }
]

AutoSamplingTheory/TechnicalLemmas/Registry.lean:448published source at 77184245109a

No declaration docstring.

def calculusMemory : List LemmaMemoryEntry := [
  {
    key := "analysis.calculus.smooth-unit-cutoff-eq-smoothTransition",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff_eq_smoothTransition",
    upstreamDecl := "GaussianSobolev.smoothCutoff_eq_smoothTransition",
    upstreamFile := "SLT/GaussianSobolevDense/Defs.lean@d0f506f; Mathlib.Analysis.Calculus.BumpFunction.InnerProduct",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["log-concave-sampling", "cutoff", "smoothTransition", "unit-scale"],
    saldUse := "log-concave sampling Ch.1 cutoff root: expose the unit cutoff through Mathlib's smooth-transition formula",
    note := "Formula leaf only. It does not assert a scaled family, derivative bounds, tail passage, weighted IBP, or invariant law."
  },
  {
    key := "analysis.calculus.smooth-unit-cutoff-contDiff",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff_contDiff",
    upstreamDecl := "GaussianSobolev.smoothCutoff_contDiff",
    upstreamFile := "SLT/GaussianSobolevDense/Defs.lean@d0f506f; Mathlib.Analysis.Calculus.BumpFunction.InnerProduct",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["log-concave-sampling", "cutoff", "ContDiff", "unit-scale"],
    saldUse := "log-concave sampling Ch.1 cutoff root: global smoothness of the reusable one-dimensional unit cutoff",
    note := "Smoothness leaf only. It gives no derivative-size estimate or integration theorem."
  },
  {
    key := "analysis.calculus.smooth-unit-cutoff-one-of-abs-le-one",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff_eq_one_of_abs_le_one",
    upstreamDecl := "GaussianSobolev.smoothCutoff_eq_one_of_le",
    upstreamFile := "SLT/GaussianSobolevDense/Defs.lean@d0f506f; Mathlib.Analysis.SpecialFunctions.SmoothTransition",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["log-concave-sampling", "cutoff", "plateau", "unit-scale"],
    saldUse := "log-concave sampling Ch.1 cutoff root: identify the unit cutoff plateau on the closed unit interval",
    note := "Unit-scale value leaf only; no scaled derivative or tail claim."
  },
  {
    key := "analysis.calculus.smooth-unit-cutoff-zero-of-two-le-abs",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff_eq_zero_of_two_le_abs",
    upstreamDecl := "GaussianSobolev.smoothCutoff_eq_zero_of_ge",
    upstreamFile := "SLT/GaussianSobolevDense/Defs.lean@d0f506f; Mathlib.Analysis.SpecialFunctions.SmoothTransition",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["log-concave-sampling", "cutoff", "support", "unit-scale"],
    saldUse := "log-concave sampling Ch.1 cutoff root: the unit cutoff vanishes beyond radius two",
    note := "Pointwise vanishing leaf only; compactness and topological support are separate leaves."
  },
  {
    key := "analysis.calculus.smooth-unit-cutoff-mem-Icc",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff_mem_Icc",
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Registry.lean:481published source at 77184245109a

Excerpt truncated; the exact source link is authoritative.

No declaration docstring.

def measureMemory : List LemmaMemoryEntry := [
  {
    key := "measure.wasserstein.chewi-definition-1-3-4",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSpace.wassersteinDistance",
    upstreamDecl := "Chewi Definition 1.3.4",
    upstreamFile := "Log-Concave Sampling, book page 20 / PDF page 32",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "Wasserstein", "W2", "quadratic-cost", "coupling", "ENNReal"],
    saldUse := "Chewi Definition 1.3.4 root: define W2 as the positive square root of quadratic Kantorovich cost",
    note := "Exact extended-real value definition; metric properties and finite-second-moment finiteness are separate theorems."
  },
  {
    key := "measure.wasserstein.chewi-display-1-3-5",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSpace.wassersteinDistance_sq",
    upstreamDecl := "Chewi display (1.3.5)",
    upstreamFile := "Log-Concave Sampling, book page 20 / PDF page 32",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "Wasserstein", "W2", "quadratic-cost", "source-display"],
    saldUse := "Chewi display (1.3.5): rewrite W2 squared as the quadratic coupling infimum",
    note := "Actual ENNReal rpow calculation; no optimal coupling is assumed."
  },
  {
    key := "measure.wasserstein.chewi-definition-1-3-12",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSpace.IsAbsolutelyContinuousFiniteSecondMoment",
    upstreamDecl := "Chewi Definition 1.3.12",
    upstreamFile := "Log-Concave Sampling, book page 25 / PDF page 37",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "Wasserstein", "P2ac", "absolute-continuity", "second-moment", "Lebesgue"],
    saldUse := "Chewi Definition 1.3.12 root: package probability normalization, finite second moment, and Lebesgue absolute continuity",
    note := "Exact measure-class definition; no Wasserstein metric, optimal map, or gradient-flow theorem is asserted."
  },
  {
    key := "measure.wasserstein.quadratic-optimal-coupling",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolation.IsQuadraticOptimalCoupling",
    upstreamDecl := "Chewi Definition 1.3.25 / quadratic Kantorovich attainment",
    upstreamFile := "Log-Concave Sampling, book page 30 / PDF page 42",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "Wasserstein", "optimal-coupling", "quadratic-cost", "attainment"],
    saldUse := "state that a prescribed coupling actually attains the quadratic Kantorovich infimum before constructing displacement interpolation",
    note := "This predicate does not prove that an optimizer exists; it records marginal feasibility and exact attainment."
  },
  {
    key := "measure.wasserstein.displacement-interpolation",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolation.displacementInterpolation",
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Registry.lean:1524published source at 77184245109a

Excerpt truncated; the exact source link is authoritative.

No declaration docstring.

def functionalInequalityMemory : List LemmaMemoryEntry := [
  {
    key := "functional-inequality.chewi-definition-1-2-19",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Generator.SatisfiesPoincare",
    upstreamDecl := "Chewi Definition 1.2.19",
    upstreamFile := "Log-Concave Sampling, book page 16 / PDF page 28",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "Poincare", "generator", "Dirichlet-form", "variance", "definition"],
    saldUse := "Chewi Definition 1.2.19 root: state the general generator Poincare inequality on every finite-integral observable",
    note := "Exact reversible-generator formulation. The gradient-energy specialization and PI-to-decay equivalence are separate theorem routes."
  },
  {
    key := "functional-inequality.chewi-definition-1-2-25",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Generator.SatisfiesLogSobolev",
    upstreamDecl := "Chewi Definition 1.2.25",
    upstreamFile := "Log-Concave Sampling, book page 18 / PDF page 30",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "log-Sobolev", "generator", "Dirichlet-form", "density", "definition"],
    saldUse := "Chewi Definition 1.2.25 root: state KL(rho mu || mu) <= (C/2) E(rho,log rho) for every admissible normalized density",
    note := "Exact density-generator formulation with positivity, normalization, and finite entropy/energy conditions explicit. KL decay is a separate theorem route."
  },
  {
    key := "gronwall.chewi-lemma-1-2-20",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.chewi_lemma_1_2_20",
    upstreamDecl := "le_gronwallBound_of_liminf_deriv_right_le / gronwallBound_ε0",
    upstreamFile := "Mathlib.Analysis.ODE.Gronwall; Log-Concave Sampling, book page 16 / PDF page 28",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "Gronwall", "differential-inequality", "exponential-bound", "Chapter-1"],
    saldUse := "Chewi Lemma 1.2.20: turn g'(t) ≤ c g(t) on [0,T] into g(t) ≤ g(0) exp(ct)",
    note := "Source-faithful differentiable scalar specialization of Mathlib's more general one-sided-slope Gronwall theorem."
  },
  {
    key := "semigroup-decay.from-arbitrary-time",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.exponential_decay_of_scaled_dissipation_from",
    upstreamDecl := "le_gronwallBound_of_liminf_deriv_right_le / time translation",
    upstreamFile := "Mathlib.Analysis.ODE.Gronwall",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "functional-inequality", "semigroup", "dissipation", "shifted-time", "exponential-decay"],
    saldUse := "propagate a coercive energy-dissipation inequality exponentially between arbitrary starting and terminal times",
    note := "Shifted-time strengthening of the zero-time Gronwall leaf; the concrete energy and dissipation remain explicit inputs."
  },
  {
    key := "semigroup-decay.converse-from-shifted-exponential",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.scaled_dissipation_of_exponential_decay",
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Registry.lean:2009published source at 77184245109a

Excerpt truncated; the exact source link is authoritative.

No declaration docstring.

def stochasticProcessMemory : List LemmaMemoryEntry := [
  {
    key := "localization.chewi-proposition-1-1-13",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalLocalizationTheorem.chewi_proposition_1_1_13",
    upstreamDecl := "Chewi Proposition 1.1.13",
    upstreamFile := "Log-Concave Sampling, book page 7 / PDF page 19",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "Ito", "localization", "stopping-time", "progressive-L2"],
    saldUse := "package the canonical energy first-hitting times, terminal convergence, and stopped global-L2 bound into the exact Chapter 1 source result",
    note := "Display (1.1.14) and Proposition 1.1.16 remain separate theorem routes; both are now compiled, so this entry records only the canonical localization component."
  },
  {
  key := "localization.chewi-display-1-1-14",
  localDecl := "AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalStoppedItoIntegral.chewi_display_1_1_14",
  upstreamDecl := "Chewi display (1.1.14)",
  upstreamFile := "Log-Concave Sampling, book page 7 / PDF page 19",
  status := LemmaMemoryStatus.formalizedLocal,
  tags := ["Chewi", "Ito", "localization", "stopped-integral", "continuous-martingale"],
  saldUse := "package each canonical energy truncation as a globally L2 Ito integrand whose Ito process is adapted, continuous, martingale, and compatible with deterministic-time restriction",
  note := "This compiles the intermediate stopped-global-Ito display. Arbitrary random-stopping consistency and cross-horizon gluing are discharged separately by Proposition 1.1.16."
},
{
  key := "localization.chewi-proposition-1-1-16",
  localDecl := "AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ChewiProposition1_1_16.chewi_proposition_1_1_16",
  upstreamDecl := "Chewi Proposition 1.1.16",
  upstreamFile := "Log-Concave Sampling, book page 7 / PDF page 19",
  status := LemmaMemoryStatus.formalizedLocal,
  tags := ["Chewi", "Ito", "local-martingale", "localization", "random-stopping", "continuous-paths"],
  saldUse := "package random-stopping consistency, cross-horizon overlap, localized martingale coherence, and pathwise gluing into the source local-Ito continuous-local-martingale result",
  note := "Uses the canonical localizers from Proposition 1.1.13; stopped-integral compatibility, stopping-graph nullity, and cross-horizon gluing are all compiled."
},
  {
    key := "localization.completed-integrand-progressive",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CompletedIntegrand.completedIntegrand_stronglyProgressive",
    upstreamDecl := "Progressiveness after completing the null bad-path set",
    upstreamFile := "Log-Concave Sampling, Proposition 1.1.13, book page 7 / PDF page 19",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "Ito", "localization", "completion", "progressive"],
    saldUse := "replace nonintegrable sample paths by zero while preserving the progressive sigma-algebra",
    note := "The source local-L2 domain assumes only almost-sure finite path energy. Usual-condition completeness makes the null replacement measurable at every filtration time."
  },
  {
    key := "localization.energy-stopped-path-bound",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.EnergyStoppedIntegrand.integral_energyStoppedIntegrand_sq_le",
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Registry.lean:2132published source at 77184245109a

Excerpt truncated; the exact source link is authoritative.

No declaration docstring.

def klDensityMemory : List LemmaMemoryEntry := [
  {
    key := "kl-density.pointwise-derivative-simplify",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.InformationTheory.KLDensity.klPointwiseDerivSimplify",
    upstreamDecl := "pointwise real-field algebra for d/ds q log(q/p)",
    upstreamFile := "local Mathlib field_simp/ring proof",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["KL", "density", "log", "pointwise-algebra"],
    saldUse := "separate KL density derivative algebra from dominated differentiation and density regularity assumptions",
    note := "Pro-assimilated leaf; positivity/nonzero and domination stay explicit."
  },
  {
    key := "kl-density.remove-mass-term",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.InformationTheory.KLDensity.klDerivativeRemoveMassTerm",
    upstreamDecl := "mass-conservation derivative simplification",
    upstreamFile := "local Mathlib HasDerivAt congruence/simp proof",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["KL", "density", "mass-conservation", "HasDerivAt"],
    saldUse := "remove the integral qdot term in KL differentiation after mass conservation is supplied",
    note := "Small derivative-target rewrite; mass conservation itself remains a separate theorem or hypothesis."
  }
]

AutoSamplingTheory/TechnicalLemmas/Registry.lean:3375published source at 77184245109a

No declaration docstring.

def renyiDensityMemory : List LemmaMemoryEntry := [
  {
    key := "renyi-density.integrand-positivity",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.InformationTheory.Renyi.renyiIntegrand_pos",
    upstreamDecl := "Real.rpow_pos_of_pos / Real.rpow_nonneg",
    upstreamFile := "Mathlib.Analysis.SpecialFunctions.Pow.Real",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "Renyi", "density", "positivity", "rpow"],
    saldUse := "Chewi DENS/FI root: expose Renyi integrand positivity before integral and derivative contracts",
    note := "Companion nonnegative theorem is `renyiIntegrand_nonneg`; full Renyi divergence remains separate."
  },
  {
    key := "renyi-density.integrand-measurable",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.InformationTheory.Renyi.measurable_renyiIntegrandENNReal",
    upstreamDecl := "Real.continuous_rpow_const / Measurable.ennreal_ofReal",
    upstreamFile := "Mathlib.Analysis.SpecialFunctions.Pow.Continuity; Mathlib.MeasureTheory.Constructions.BorelSpace.Real",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "Renyi", "density", "measurability", "ENNReal"],
    saldUse := "Chewi DENS/FI root: turn measurable density representatives into a measurable Renyi lintegrand",
    note := "Requires order `a ∈ [0,1]`; representative choice and absolute continuity stay explicit."
  },
  {
    key := "renyi-density.integral-finite-envelope",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.InformationTheory.Renyi.lintegral_renyiIntegrandENNReal_ne_top_of_ae_le",
    upstreamDecl := "lintegral_mono_ae / ne_top_of_le_ne_top",
    upstreamFile := "Mathlib.MeasureTheory.Integral.Lebesgue.Basic",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "Renyi", "density", "lintegral", "envelope", "finite"],
    saldUse := "Chewi DENS/FI root: reduce Renyi integrability to a finite ENNReal envelope",
    note := "This mirrors the Gibbs finite-envelope contract and keeps tail/domination estimates outside the algebra leaf."
  },
  {
    key := "renyi-density.pointwise-derivative",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.InformationTheory.Renyi.hasDerivAt_renyiIntegrand",
    upstreamDecl := "HasDerivAt.rpow_const / HasDerivAt.mul",
    upstreamFile := "Mathlib.Analysis.SpecialFunctions.Pow.Deriv",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "Renyi", "density", "pointwise-derivative", "rpow"],
    saldUse := "Chewi chapter 6 root: isolate pointwise Renyi derivative algebra before dominated differentiation under the integral",
    note := "Positivity/nonzero, domination, and path-space regularity remain explicit source contracts."
  }
]

AutoSamplingTheory/TechnicalLemmas/Registry.lean:3398published source at 77184245109a

No declaration docstring.

def variationalMemory : List LemmaMemoryEntry := [
  {
    key := "dv.scaled-test.energy-bound",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.InformationTheory.DonskerVaradhan.dvVariationalScaledTestEnergyBound",
    upstreamDecl := "Donsker--Varadhan one-sided variational consequence",
    upstreamFile := "Boucheron-style cited result / future SLT entropy-duality port",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["DV", "KL", "energy"],
    saldUse := "convert finite log-mgf and KL hypotheses into residual energy bounds",
    note := "Small compiled consequence; full DV theorem remains a cited-result obligation."
  },
  {
    key := "lsi.sqrt-density.fisher-chain",
    localDecl := "AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainIntegralHandoffScalar",
    upstreamDecl := "LSI density and Fisher-information bookkeeping",
    upstreamFile := "Mathlib/SLT-inspired entropy and LSI proof shape",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["LSI", "FI", "density"],
    saldUse := "bookkeeping for LSI-to-KL/FI handoff after density assumptions are supplied",
    note := "Compiled scalar/integral algebra; full LSI analytic theorem remains an obligation."
  },
  {
    key := "poincare.variance",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance",
    upstreamDecl := "MeasureTheory.integral",
    upstreamFile := "Mathlib.MeasureTheory.Integral.Bochner.Basic",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "chapter-2", "Poincare", "variance", "definition"],
    saldUse := "shared Chapter 2 variance interface with the centering convention visible in Lean",
    note := "The integral is totalized; consumers must carry the separate admissibility hypotheses."
  },
  {
    key := "poincare.dirichlet-energy",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.dirichletEnergy",
    upstreamDecl := "Analysis.Calculus.gradient / MeasureTheory.integral",
    upstreamFile := "AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient; Mathlib.MeasureTheory.Integral.Bochner.Basic",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "chapter-2", "Poincare", "Dirichlet-energy", "definition"],
    saldUse := "shared gradient-energy term for Poincare statements and later semigroup dissipation leaves",
    note := "This is the Euclidean/inner-product energy interface, not a closed Dirichlet-form construction."
  },
  {
    key := "poincare.admissible",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.Admissible",
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Registry.lean:3441published source at 77184245109a

Excerpt truncated; the exact source link is authoritative.

No declaration docstring.

def geometryMemory : List LemmaMemoryEntry := [
  {
    key := "geometry.chewi-definition-1-3-26",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.Geometry.GeodesicConvexity.IsAlphaGeodesicallyConvex",
    upstreamDecl := "Chewi Definition 1.3.26, condition 1",
    upstreamFile := "Log-Concave Sampling, book page 31 / PDF page 43",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "geodesic-convexity", "metric-space", "interpolation", "definition"],
    saldUse := "Chewi Definition 1.3.26 root: state alpha-geodesic convexity through the endpoint interpolation inequality along every selected geodesic",
    note := "The geodesic predicate remains an explicit parameter so Riemannian and Wasserstein realizations can supply their own constant-speed/domain conditions."
  },
  {
    key := "geometry.chewi-display-1-4-7",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.Geometry.GeodesicConvexity.firstOrder_geodesicConvexity",
    upstreamDecl := "HasDerivAt.tendsto_slope / le_of_tendsto_of_tendsto",
    upstreamFile := "Mathlib.Analysis.Calculus.Deriv.Slope; Chewi display (1.4.7)",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "geodesic-convexity", "first-order-condition", "derivative", "Wasserstein"],
    saldUse := "Derive the first-order alpha-convexity inequality from the endpoint chord condition along a differentiable geodesic",
    note := "The proof takes the positive-time secant-slope limit. Concrete Riemannian or Wasserstein geometry must identify the path derivative with its gradient pairing."
  },
  {
    key := "geometry.chewi-definition-1-3-16",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.Geometry.MetricCurve.IsAbsolutelyContinuousMetricCurve",
    upstreamDecl := "Chewi Definition 1.3.16 (informal)",
    upstreamFile := "Log-Concave Sampling, book page 26 / PDF page 38",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "metric-derivative", "absolutely-continuous-curve", "Wasserstein", "definition"],
    saldUse := "Chewi Definition 1.3.16 root: require a finite nonnegative punctured-neighborhood metric derivative at almost every time",
    note := "Matches the source's explicitly informal definition. The standard upper-gradient characterization and Wasserstein specialization remain theorem routes."
  },
  {
    key := "geometry.euclidean-space.inner-toLp-toLp-sum",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.Geometry.EuclideanSpaceCoordinates.euclideanSpace_inner_toLp_toLp_eq_sum_mul",
    upstreamDecl := "PiLp.inner_apply",
    upstreamFile := "Mathlib.Analysis.InnerProductSpace.PiL2",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Chewi", "EuclideanSpace", "inner-product", "coordinates", "WithLp.toLp", "finite-dimensional"],
    saldUse := "Chewi GAUSS/SDE root: bridge coordinate gradient representatives to Mathlib `EuclideanSpace` inner-product notation",
    note := "Pure finite-dimensional coordinate identity; it does not define gradients, divergence, Laplacian, or analytic regularity."
  },
  {
    key := "geometry.euclidean-space.inner-sum",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.Geometry.EuclideanSpaceCoordinates.euclideanSpace_inner_eq_sum_mul",
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Registry.lean:3554published source at 77184245109a

Excerpt truncated; the exact source link is authoritative.

No declaration docstring.

def saldExtractedMemory : List LemmaMemoryEntry := [
  {
    key := "sald.gronwall.scalar-rewrites",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.SALDExtracted.gronwallExpProductRewriteScalar",
    upstreamDecl := "SALD appendix Gronwall proof plus elementary exponential algebra",
    upstreamFile := "AutoSamplingTheory/SALD.lean",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Gronwall", "scalar-algebra", "SALD-extracted"],
    saldUse := "forward-KL and discrete forward-KL Gronwall display algebra",
    note := "Compiled in SALD and exposed through TechnicalLemmas.SALDExtracted."
  },
  {
    key := "sald.em-endpoint-law-handoff",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.SALDExtracted.discreteForwardKlEmEndpointLawPairHandoff",
    upstreamDecl := "SALD discrete EM endpoint law bookkeeping",
    upstreamFile := "AutoSamplingTheory/SALD.lean",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Euler-Maruyama", "endpoint-law", "SALD-extracted"],
    saldUse := "endpoint-law pair handoff for discrete SALD/VA-SALD proofs",
    note := "SALD-derived local theorem exposed as a searchable memory item."
  },
  {
    key := "sald.brownian-normalization-bridges",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.SALDExtracted.selectedWeakTestNormalizedCoordinateLawOfStdGaussianVectorLaw",
    upstreamDecl := "SALD Brownian/Ito normalized-coordinate law bridge",
    upstreamFile := "AutoSamplingTheory/SALD.lean",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Brownian", "Ito", "Gaussian", "SALD-extracted"],
    saldUse := "active Brownian/Ito scalar generator backend and coordinate variance leaves",
    note := "Domain-specific SALD bridge; can be generalized later if reused."
  },
  {
    key := "sald.remainder-meas-gaussian-law",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.SALDExtracted.selectedWeakTestRemainderMeasOfStdGaussianVectorLaw",
    upstreamDecl := "SALD Brownian/Ito normalized-remainder measurability bridge",
    upstreamFile := "AutoSamplingTheory/SALD.lean",
    status := LemmaMemoryStatus.formalizedLocal,
    tags := ["Brownian", "Ito", "Gaussian", "measurability", "SALD-extracted"],
    saldUse := "discharge hRemainderMeas in the active Brownian/Ito Taylor moment backend",
    note := "Cycle 194 bridge transporting AEStronglyMeasurable across the normalized coordinate-law and variance equalities."
  },
  {
    key := "sald.remainder-bound-gaussian-law",
    localDecl := "AutoSamplingTheory.TechnicalLemmas.SALDExtracted.selectedWeakTestRemainderBoundOfStdGaussianVectorLaw",
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Registry.lean:3967published source at 77184245109a

Excerpt truncated; the exact source link is authoritative.

No declaration docstring.

def portQueueMemory : List LemmaMemoryEntry := [
  {
    key := "dv.entropy-duality",
    localDecl := "",
    upstreamDecl := "entropy_duality",
    upstreamFile := "SLT/GaussianLSI/DualityEntropy.lean",
    status := LemmaMemoryStatus.portCandidate,
    tags := ["DV", "entropy", "KL"],
    saldUse := "Donsker--Varadhan variational backend for KL energy bounds",
    note := "Port only when DV becomes the active dynamic leaf."
  },
  {
    key := "lsi.product-gaussian",
    localDecl := "",
    upstreamDecl := "gaussian_logSobolev_W12_pi",
    upstreamFile := "SLT/GaussianLSI/TensorizedGLSI.lean",
    status := LemmaMemoryStatus.portCandidate,
    tags := ["LSI", "Gaussian", "product"],
    saldUse := "LSI-to-KL/FI backend when the faithful proof reaches this cited-result boundary",
    note := "Large theorem; keep as queue entry until a local ASTIS declaration compiles."
  }
]

AutoSamplingTheory/TechnicalLemmas/Registry.lean:4040published source at 77184245109a

No declaration docstring.

def technicalLemmaMemory : List LemmaMemoryEntry :=
  analysisMemory ++ gaussianMemory ++ taylorMemory ++ calculusMemory ++ measureMemory ++ functionalInequalityMemory ++ stochasticProcessMemory ++
    klDensityMemory ++ renyiDensityMemory ++ variationalMemory ++ geometryMemory ++
    saldExtractedMemory ++ portQueueMemory

AutoSamplingTheory/TechnicalLemmas/Registry.lean:4063published source at 77184245109a

No declaration docstring.

def formalizedTechnicalLemmaCount : Nat :=
  (technicalLemmaMemory.filter fun entry =>
    entry.status == LemmaMemoryStatus.formalizedLocal).length

end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Registry.lean:4068published source at 77184245109a