Markov Semigroup Theory

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem fundamental_integration_by_parts
    [MeasurableSpace X]
    (mu : Measure X) (generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
    (f g : X → ℝ)
    (hLfg : Integrable (generator (f * g)) mu)
    (hfLg : Integrable (fun x => f x * generator g x) mu)
    (hgLf : Integrable (fun x => g x * generator f x) mu)
    (hstationary : (∫ x, generator (f * g) x ∂mu) = 0)
    (hsymmetric :
      (∫ x, f x * generator g x ∂mu) =
        ∫ x, g x * generator f x ∂mu) :
    FunctionalInequalities.Generator.dirichletForm mu generator f g =
        FunctionalInequalities.Generator.dirichletForm mu generator g f ∧
      FunctionalInequalities.Generator.dirichletForm mu generator f g =
        ∫ x, carreDuChamp generator f g x ∂mu := by
  have hsub : Integrable
      (fun x => generator (f * g) x - f x * generator g x) mu :=
    hLfg.sub hfLg
  have hgammaIntegral :
      (∫ x, carreDuChamp generator f g x ∂mu) =
        (2 : ℝ)⁻¹ *
          ((∫ x, generator (f * g) x ∂mu) -
            (∫ x, f x * generator g x ∂mu) -
            ∫ x, g x * generator f x ∂mu) := by
    change
      (∫ x, (2 : ℝ)⁻¹ *
        (generator (f * g) x - f x * generator g x -
          g x * generator f x) ∂mu) = _
    rw [integral_const_mul,
      integral_sub hsub hgLf, integral_sub hLfg hfLg]
  constructor
  · simp only [FunctionalInequalities.Generator.dirichletForm]
    rw [hsymmetric]
  · simp only [FunctionalInequalities.Generator.dirichletForm]
    rw [hgammaIntegral, hstationary, hsymmetric]
    ring

/-- Chewi Corollary 1.2.15: the negative reversible generator has a
nonnegative quadratic form once Gamma is pointwise nonnegative. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem negativeGenerator_quadratic_nonneg
    [MeasurableSpace X]
    (mu : Measure X) (generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
    (f : X → ℝ)
    (hLf2 : Integrable (generator (f * f)) mu)
    (hfLf : Integrable (fun x => f x * generator f x) mu)
    (hstationary : (∫ x, generator (f * f) x ∂mu) = 0)
    (hgamma : ∀ x, 0 ≤ carreDuChamp generator f f x) :
    0 ≤ FunctionalInequalities.Generator.dirichletForm mu generator f f := by
  have hibp := fundamental_integration_by_parts mu generator f f
    hLf2 hfLf hfLf hstationary rfl
  rw [hibp.2]
  exact integral_nonneg_of_ae (Filter.Eventually.of_forall hgamma)

end CarreDuChamp
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

def SatisfiesPoincare
    (mu : Measure E) (generator : (E → ℝ) → E → ℝ)
    (C : ℝ) : Prop :=
  IsProbabilityMeasure mu ∧ 0 < C ∧
    ∀ f : E → ℝ, PoincareAdmissible mu generator f →
      variance mu f ≤ C * dirichletForm mu generator f f

/-- Relative entropy of a density `rho` with respect to its reference
probability measure.  Mathlib's totalized `Real.log 0 = 0` gives the standard
zero-density convention in the product `rho * log rho`. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

def SatisfiesLogSobolev
    (mu : Measure E) (generator : (E → ℝ) → E → ℝ)
    (C : ℝ) : Prop :=
  IsProbabilityMeasure mu ∧ 0 < C ∧
    ∀ rho : E → ℝ, LogSobolevAdmissible mu generator rho →
      densityEntropy mu rho ≤
        (C / 2) * dirichletForm mu generator rho (fun x => Real.log (rho x))

end Generator
end FunctionalInequalities
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

def markovOperator {K : ℝ≥0 → Kernel E E}
    (_hK : TransitionKernelContract K) (t : ℝ≥0) :
    MeasurableENNReal E → MeasurableENNReal E :=
  fun f => by
    exact ⟨fun x => ∫⁻ y, f y ∂K t x, f.2.lintegral_kernel⟩

/-- A Markov operator preserves constant nonnegative observables. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

structure IntegratedSemigroupGeneratorContract {E : Type*} [MeasurableSpace E]
    (P : ℝ → (E → ℝ) → E → ℝ)
    (generator : (E → ℝ) → E → ℝ)
    (domain : Set (E → ℝ))
    (μ : Measure E) : Prop where
  map_zero : ∀ f, P 0 f = f
  map_add : ∀ s, 0 ≤ s → ∀ t, 0 ≤ t → ∀ f,
    P (s + t) f = P s (P t f)
  orbit_mem_domain : ∀ t, 0 ≤ t → ∀ f ∈ domain, P t f ∈ domain
  pairing_continuousOn : ∀ t, 0 ≤ t → ∀ f ∈ domain,
    ContinuousOn (fun s => ∫ x, P s f x ∂μ) (Set.Icc 0 t)
  pairing_hasDerivWithinAt : ∀ t, 0 ≤ t → ∀ f ∈ domain,
    HasDerivWithinAt
      (fun s => ∫ x, P s f x ∂μ)
      (∫ x, generator (P t f) x ∂μ) (Set.Ici t) t

/-- A semigroup is invariant on its declared generator domain when integrated
generator action vanishes throughout that domain.

This theorem is the operator-domain-to-invariance bridge.  All analytic
content is visible in `IntegratedSemigroupGeneratorContract`; in particular,
the right derivative of the integral pairing and preservation of the domain
are not inferred from a formal differential expression. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem isInvariantOn_of_integral_generator_eq_zero
    {E : Type*} [MeasurableSpace E]
    {P : ℝ → (E → ℝ) → E → ℝ}
    {generator : (E → ℝ) → E → ℝ}
    {domain : Set (E → ℝ)} {μ : Measure E}
    (hsemigroup : IntegratedSemigroupGeneratorContract P generator domain μ)
    (hgenerator_zero : ∀ f ∈ domain, ∫ x, generator f x ∂μ = 0) :
    IsInvariantOn P μ domain := by
  intro t ht f hf
  have hconstant := constant_of_has_deriv_right_zero
    (hsemigroup.pairing_continuousOn t ht f hf) (fun s hs => by
      have hs0 : 0 ≤ s := hs.1
      simpa [hgenerator_zero (P s f)
        (hsemigroup.orbit_mem_domain s hs0 f hf)] using
        hsemigroup.pairing_hasDerivWithinAt s hs0 f hf)
  have htmem : t ∈ Set.Icc (0 : ℝ) t := ⟨ht, le_rfl⟩
  simpa [hsemigroup.map_zero f] using hconstant t htmem

/-- Move a supplied sample-space generator derivative to a named law path.

In SDE applications, `hderiv` is usually the Ito-generator derivative for a
test function composed with a process, while `hDrift` and `hDiffusion` identify
the sample drift and diffusion-generator terms with law-level weak-test
integrals.  The lemma proves only the reusable rewrite; it does not construct
the process, conditional drift, or Ito theorem.
-/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem chewi_lemma_1_2_2 {K : ℝ≥0 → Kernel E E}
    (hK : TransitionKernelContract K) :
    markovOperator hK 0 = id ∧
      ∀ s t : ℝ≥0,
        markovOperator hK s ∘ markovOperator hK t =
            markovOperator hK (s + t) ∧
          markovOperator hK t ∘ markovOperator hK s =
            markovOperator hK (s + t) := by
  constructor
  · exact markovOperator_zero hK
  · intro s t
    constructor
    · exact markovOperator_comp hK s t
    · simpa [add_comm] using markovOperator_comp hK t s

end

end MarkovSemigroup
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem markovOperator_const {K : ℝ≥0 → Kernel E E}
    (hK : TransitionKernelContract K) (t : ℝ≥0) (c : ℝ≥0∞) :
    markovOperator hK t (MeasurableENNReal.const c) =
      MeasurableENNReal.const c := by
  apply Subtype.ext
  funext x
  change (∫⁻ _y, c ∂K t x) = c
  let : IsMarkovKernel (K t) := hK.isMarkov t
  simp

/-- Markov integration is monotone in the observable. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem markovOperator_apply_mono {K : ℝ≥0 → Kernel E E}
    (hK : TransitionKernelContract K) (t : ℝ≥0)
    {f g : MeasurableENNReal E} (hfg : ∀ y, f y ≤ g y) (x : E) :
    markovOperator hK t f x ≤ markovOperator hK t g x := by
  change (∫⁻ y, f y ∂K t x) ≤ ∫⁻ y, g y ∂K t x
  exact lintegral_mono hfg

/-- At time zero, the transition-kernel Markov operator is the identity. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem norm_fellerOperator_apply_le {K : ℝ≥0 → Kernel E E}
    (hK : FellerTransitionKernelContract K) (t : ℝ≥0)
    (f : E →ᵇ ℝ) :
    ‖fellerOperator hK t f‖ ≤ ‖f‖ := by
  exact BoundedContinuousFunction.norm_ofNormedAddCommGroup_le
    (hK.mapsContinuous t f) (norm_nonneg f)
    (norm_kernelIntegral_le hK t f)

/-- Jensen's inequality for the square under a Feller Markov operator:
`(P_t f x)^2 ≤ P_t(f^2)(x)`. This is equation (1.2.11) in Chewi's
2026-08-09 edition. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem fellerOperator_add {K : ℝ≥0 → Kernel E E}
    (hK : FellerTransitionKernelContract K) (s t : ℝ≥0) :
    fellerOperator hK (s + t) =
      (fellerOperator hK s).comp (fellerOperator hK t) := by
  let : IsMarkovKernel (K s) := hK.toTransitionKernelContract.isMarkov s
  let : IsMarkovKernel (K t) := hK.toTransitionKernelContract.isMarkov t
  ext f x
  change (∫ z, f z ∂K (s + t) x) =
    ∫ y, (∫ z, f z ∂K t y) ∂K s x
  rw [hK.toTransitionKernelContract.chapmanKolmogorov s t]
  exact Kernel.integral_comp
    (integrable_boundedContinuousFunction f ((K t ∘ₖ K s) x))

/-- A Feller transition-kernel contract therefore supplies the exact
continuous-linear semigroup consumed by the right-generator development. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

def continuousLinearSemigroupOfFeller {K : ℝ≥0 → Kernel E E}
    (hK : FellerTransitionKernelContract K) :
    ContinuousLinearSemigroup (E →ᵇ ℝ) where
  op := fellerOperator hK
  op_zero := fellerOperator_zero hK
  op_add := fellerOperator_add hK

@[simp]

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem StronglyContinuousSemigroup.tendsto_op_add
    (S : StronglyContinuousSemigroup M) (t : ℝ≥0) (f : M) :
    Tendsto (fun h : ℝ≥0 => S.op (t + h) f) (𝓝 0) (𝓝 (S.op t f)) := by
  have hop : Tendsto (S.op t) (𝓝 f) (𝓝 (S.op t f)) :=
    (S.op t).continuous.continuousAt
  have hmapped :
      Tendsto (fun h : ℝ≥0 => S.op t (S.op h f))
        (𝓝 0) (𝓝 (S.op t f)) :=
    hop.comp (S.stronglyContinuousAtZero f)
  simpa only [ContinuousLinearSemigroup.op_add_apply] using hmapped

/-- The zero vector has generator value zero. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem chewi_lemma_1_2_2 {K : ℝ≥0 → Kernel E E}
    (hK : TransitionKernelContract K) :
    markovOperator hK 0 = id ∧
      ∀ s t : ℝ≥0,
        markovOperator hK s ∘ markovOperator hK t =
            markovOperator hK (s + t) ∧
          markovOperator hK t ∘ markovOperator hK s =
            markovOperator hK (s + t) := by
  constructor
  · exact markovOperator_zero hK
  · intro s t
    constructor
    · exact markovOperator_comp hK s t
    · simpa [add_comm] using markovOperator_comp hK t s

end

end MarkovSemigroup
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

def HasRightGeneratorAt (S : ContinuousLinearSemigroup M)
    (f g : M) : Prop :=
  Tendsto (fun h : ℝ≥0 => rightDifferenceQuotient S h f)
    (nhdsWithin 0 (Ioi 0)) (𝓝 g)

/-- The domain of the right generator in the chosen norm topology. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem kolmogorov_backward_right
    (S : ContinuousLinearSemigroup M) {f g : M}
    (hfg : HasRightGeneratorAt S f g) (t : ℝ≥0) :
    HasRightGeneratorAt S (S.op t f) (S.op t g) ∧
      Tendsto (fun h : ℝ≥0 => rightOrbitDifferenceQuotient S t h f)
        (nhdsWithin 0 (Ioi 0)) (𝓝 (S.op t g)) := by
  have hmap := hfg.map t
  constructor
  · exact hmap
  · simpa only [HasRightGeneratorAt, rightOrbitDifferenceQuotient_eq] using hmap

end

end OperatorGenerator
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem weakGeneratorFromSampleDerivative {Ω E : Type*}
    [MeasurableSpace Ω] [MeasurableSpace E]
    {P : Measure Ω} {X : ℝ → Ω → E} {ρ : ℝ → Measure E}
    {φ driftTerm diffusionTerm : E → ℝ}
    {sampleDrift sampleDiffusion : Ω → ℝ} {s0 σ : ℝ}
    (hρ : ∀ s, ρ s = Measure.map (X s) P)
    (hX : ∀ s, AEMeasurable (X s) P)
    (hφ : ∀ s, AEStronglyMeasurable φ (ρ s))
    (hderiv :
      HasDerivAt (fun s => ∫ ω, φ (X s ω) ∂P)
        ((∫ ω, sampleDrift ω ∂P) +
          (σ ^ 2 / 2) * (∫ ω, sampleDiffusion ω ∂P)) s0)
    (hDrift :
      (∫ ω, sampleDrift ω ∂P) = ∫ x, driftTerm x ∂ρ s0)
    (hDiffusion :
      (∫ ω, sampleDiffusion ω ∂P) = ∫ x, diffusionTerm x ∂ρ s0) :
    HasDerivAt (fun s => ∫ x, φ x ∂ρ s)
      ((∫ x, driftTerm x ∂ρ s0) +
        (σ ^ 2 / 2) * (∫ x, diffusionTerm x ∂ρ s0)) s0 := by
  have hbase :
      HasDerivAt (fun s => ∫ x, φ x ∂ρ s)
        ((∫ ω, sampleDrift ω ∂P) +
          (σ ^ 2 / 2) * (∫ ω, sampleDiffusion ω ∂P)) s0 :=
    AutoSamplingTheory.lawIntegralHasDerivAtOfMeasureMapEqAndSample
      (P := P) (X := X) (ρ := ρ) (φ := φ)
      hρ hX hφ hderiv
  simpa [hDrift, hDiffusion] using hbase

end WeakGenerator
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

def continuousLinearSemigroupOfFeller {K : ℝ≥0 → Kernel E E}
    (hK : FellerTransitionKernelContract K) :
    ContinuousLinearSemigroup (E →ᵇ ℝ) where
  op := fellerOperator hK
  op_zero := fellerOperator_zero hK
  op_add := fellerOperator_add hK

@[simp]

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem generatorDomain_map
    (S : ContinuousLinearSemigroup M) {f : M}
    (hf : f ∈ generatorDomain S) (t : ℝ≥0) :
    S.op t f ∈ generatorDomain S := by
  rcases hf with ⟨g, hfg⟩
  exact ⟨S.op t g, hfg.map t⟩

/-- The forward right difference quotient of the semigroup orbit at time `t`. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem kolmogorov_backward_right
    (S : ContinuousLinearSemigroup M) {f g : M}
    (hfg : HasRightGeneratorAt S f g) (t : ℝ≥0) :
    HasRightGeneratorAt S (S.op t f) (S.op t g) ∧
      Tendsto (fun h : ℝ≥0 => rightOrbitDifferenceQuotient S t h f)
        (nhdsWithin 0 (Ioi 0)) (𝓝 (S.op t g)) := by
  have hmap := hfg.map t
  constructor
  · exact hmap
  · simpa only [HasRightGeneratorAt, rightOrbitDifferenceQuotient_eq] using hmap

end

end OperatorGenerator
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem hasRightGeneratorAt_unique
    {S : ContinuousLinearSemigroup M} {f g₁ g₂ : M}
    (hg₁ : HasRightGeneratorAt S f g₁)
    (hg₂ : HasRightGeneratorAt S f g₂) :
    g₁ = g₂ := by
  unfold HasRightGeneratorAt at hg₁ hg₂
  exact tendsto_nhds_unique hg₁ hg₂

/-- Generator limits add. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

def generatorDomainSubmodule (S : ContinuousLinearSemigroup M) :
    Submodule ℝ M where
  carrier := generatorDomain S
  zero_mem' := ⟨0, hasRightGeneratorAt_zero S⟩
  add_mem' := by
    intro f g hf hg
    rcases hf with ⟨Af, hf⟩
    rcases hg with ⟨Ag, hg⟩
    exact ⟨Af + Ag, hasRightGeneratorAt_add hf hg⟩
  smul_mem' := by
    intro c f hf
    rcases hf with ⟨Af, hf⟩
    exact ⟨c • Af, hasRightGeneratorAt_smul hf c⟩

/-- The canonical right-generator value on its submodule domain. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

noncomputable def rightGenerator (S : ContinuousLinearSemigroup M) :
    generatorDomainSubmodule S →ₗ[ℝ] M where
  toFun := rightGeneratorValue S
  map_add' := rightGeneratorValue_add S
  map_smul' := rightGeneratorValue_smul S

/-- The canonical generator commutes with the semigroup on its invariant
domain. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem rightGenerator_map
    (S : ContinuousLinearSemigroup M) (t : ℝ≥0)
    (f : generatorDomainSubmodule S) :
    rightGenerator S
        ⟨S.op t (f : M), generatorDomain_map S f.property t⟩ =
      S.op t (rightGenerator S f) := by
  apply hasRightGeneratorAt_unique
  · exact rightGeneratorValue_spec S
      ⟨S.op t (f : M), generatorDomain_map S f.property t⟩
  · exact (rightGeneratorValue_spec S f).map t

/-- Chewi's right Kolmogorov backward equation using the canonical bundled
generator rather than an existential generator witness. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem kolmogorov_backward_right_generator
    (S : ContinuousLinearSemigroup M)
    (f : generatorDomainSubmodule S) (t : ℝ≥0) :
    Tendsto
      (fun h : ℝ≥0 => rightOrbitDifferenceQuotient S t h (f : M))
      (nhdsWithin 0 (Ioi 0))
      (𝓝 (S.op t (rightGenerator S f))) := by
  exact (kolmogorov_backward_right S (rightGeneratorValue_spec S f) t).2

end

end OperatorGeneratorDomain
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

def IsReversible (S : ContinuousLinearSemigroup H) : Prop :=
  ∀ (t : ℝ≥0) (f g : H),
    inner ℝ (S.op t f) g = inner ℝ f (S.op t g)

/-- The constant identity semigroup is reversible on every real inner-product
space. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem sq_fellerOperator_apply_le {K : ℝ≥0 → Kernel E E}
    (hK : FellerTransitionKernelContract K) (t : ℝ≥0)
    (f : E →ᵇ ℝ) (x : E) :
    (fellerOperator hK t f x) ^ 2 ≤
      fellerOperator hK t (f * f) x := by
  let : IsMarkovKernel (K t) := hK.toTransitionKernelContract.isMarkov t
  have hsquare : Integrable ((fun r : ℝ => r ^ 2) ∘ fun y => f y) (K t x) := by
    simpa [Function.comp_def, pow_two] using
      (integrable_boundedContinuousFunction (f * f) (K t x))
  have hJensen :=
    (even_two.convexOn_pow : ConvexOn ℝ Set.univ fun r : ℝ => r ^ 2).map_integral_le
      (continuousOn_pow 2) isClosed_univ
      (ae_of_all _ fun y => Set.mem_univ (f y))
      (integrable_boundedContinuousFunction f (K t x))
      hsquare
  simpa [Function.comp_def, pow_two] using hJensen

/-- The zero-time Feller operator is the identity continuous linear map. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

def carreDuChamp
    (generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
    (f g : X → ℝ) : X → ℝ :=
  fun x => (2 : ℝ)⁻¹ *
    (generator (f * g) x - f x * generator g x - g x * generator f x)

/-- The carre du champ is symmetric in its observable arguments. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem carreDuChamp_nonneg_of_markov_jensen_rightGenerator
    (P : ℝ≥0 → (X → ℝ) → X → ℝ)
    (generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
    (f : X → ℝ) (x : X)
    (hjensen : ∀ h : ℝ≥0, 0 < h → (P h f x) ^ 2 ≤ P h (f * f) x)
    (hf : Tendsto
      (fun h : ℝ≥0 => (P h f x - f x) / (h : ℝ))
      (𝓝[>] 0) (𝓝 (generator f x)))
    (hf2 : Tendsto
      (fun h : ℝ≥0 => (P h (f * f) x - (f x) ^ 2) / (h : ℝ))
      (𝓝[>] 0) (𝓝 (generator (f * f) x)))
    (hcontinuous : Tendsto (fun h : ℝ≥0 => P h f x)
      (𝓝[>] 0) (𝓝 (f x))) :
    0 ≤ carreDuChamp generator f f x := by
  let gap : ℝ≥0 → ℝ := fun h =>
    (P h (f * f) x - (P h f x) ^ 2) / (2 * (h : ℝ))
  have hgap_nonneg : ∀ᶠ h in 𝓝[>] (0 : ℝ≥0), 0 ≤ gap h := by
    filter_upwards [self_mem_nhdsWithin] with h hh
    have hh0 : 0 < h := by simpa only [mem_Ioi] using hh
    exact div_nonneg (sub_nonneg.mpr (hjensen h hh0)) (by positivity)
  have hrewrite : ∀ᶠ h in 𝓝[>] (0 : ℝ≥0),
      gap h =
        (2 : ℝ)⁻¹ * ((P h (f * f) x - (f x) ^ 2) / (h : ℝ)) -
        (2 : ℝ)⁻¹ * (((P h f x - f x) / (h : ℝ)) *
          (P h f x + f x)) := by
    filter_upwards [self_mem_nhdsWithin] with h hh
    have hh0 : (h : ℝ) ≠ 0 := by
      have : 0 < h := by simpa only [mem_Ioi] using hh
      exact_mod_cast this.ne'
    dsimp [gap]
    field_simp
    ring
  have hlimit : Tendsto gap (𝓝[>] (0 : ℝ≥0))
      (𝓝 (carreDuChamp generator f f x)) := by
    have hconst : Tendsto (fun _ : ℝ≥0 => f x)
        (nhdsWithin 0 (Set.Ioi 0)) (nhds (f x)) :=
      tendsto_const_nhds
    have hsum : Tendsto (fun h : ℝ≥0 => P h f x + f x)
        (nhdsWithin 0 (Set.Ioi 0)) (nhds (f x + f x)) :=
      hcontinuous.add hconst
    have hprod := hf.mul hsum
    have hcombined := (hf2.const_mul (2 : ℝ)⁻¹).sub
      (hprod.const_mul (2 : ℝ)⁻¹)
    have hvalue :
        (2 : ℝ)⁻¹ * generator (f * f) x -
            (2 : ℝ)⁻¹ * (generator f x * (f x + f x)) =
          carreDuChamp generator f f x := by
      simp only [carreDuChamp]
      ring
    have htarget : Tendsto
        (fun h : ℝ≥0 =>
          (2 : ℝ)⁻¹ * ((P h (f * f) x - (f x) ^ 2) / (h : ℝ)) -
          (2 : ℝ)⁻¹ * (((P h f x - f x) / (h : ℝ)) *
            (P h f x + f x)))
        (𝓝[>] 0) (𝓝 (carreDuChamp generator f f x)) := by
      rw [← hvalue]
      exact hcombined
    exact htarget.congr' (hrewrite.mono fun h hh => hh.symm)
  exact isClosed_Ici.mem_of_tendsto hlimit hgap_nonneg

/-- Chewi Theorem 1.2.14: stationarity and generator symmetry imply the
fundamental integration-by-parts identity between the Dirichlet form and the
integrated carre du champ.

The three integrability hypotheses are the exact terms expanded from Gamma;
they prevent the totalized Bochner integral from hiding a domain failure. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem langevinCarreDuChamp_eq_inner
    {n : ℕ}
    (V f g : EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
    (hf : ContDiff ℝ 2 f) (hg : ContDiff ℝ 2 g)
    (x : EuclideanSpace ℝ (Fin (n + 1))) :
    (2 : ℝ)⁻¹ *
        (LangevinGenerator.operator V (f * g) x -
          f x * LangevinGenerator.operator V g x -
          g x * LangevinGenerator.operator V f x) =
      inner ℝ (gradient f x) (gradient g x) := by
  have hf1 : Differentiable ℝ f := hf.differentiable (by norm_num)
  have hg1 : Differentiable ℝ g := hg.differentiable (by norm_num)
  simp only [LangevinGenerator.operator]
  rw [laplacian_mul f g hf hg x, gradient_mul f g hf1 hg1 x]
  simp only [inner_add_right, real_inner_smul_right]
  ring

/-- Diagonal form of Chewi Example 1.2.17. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

def iteratedCarreDuChamp
    (generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
    (f g : X → ℝ) : X → ℝ :=
  fun x => (2 : ℝ)⁻¹ *
    (generator (carreDuChamp generator f g) x
      - carreDuChamp generator f (generator g) x
      - carreDuChamp generator g (generator f) x)

/-- The iterated carre du champ inherits symmetry from the first one. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

def SatisfiesBakryEmery
    (generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
    (alpha : ℝ) : Prop :=
  0 < alpha ∧ ∀ (f : X → ℝ) (x : X),
    alpha * carreDuChamp generator f f x ≤
      iteratedCarreDuChamp generator f f x

/-- Chewi Lemma 1.2.13: the Markov-semigroup Jensen inequality implies
nonnegativity of the carre du champ after taking the right-generator limit.

The theorem is pointwise.  `hf` and `hf2` are the actual right difference-
quotient limits for `f` and `f²`; `hcontinuous` is strong/right continuity of
the orbit at the selected state. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem chewi_lemma_1_2_20
    {T c : ℝ} (_hT : 0 < T) (g : ℝ → ℝ)
    (hg : Differentiable ℝ g)
    (hbound : ∀ t ∈ Icc (0 : ℝ) T, deriv g t ≤ c * g t)
    {t : ℝ} (ht : t ∈ Icc (0 : ℝ) T) :
    g t ≤ g 0 * Real.exp (c * t) := by
  have hgronwall :=
    le_gronwallBound_of_liminf_deriv_right_le
      (f := g)
      (f' := deriv g)
      (δ := g 0)
      (K := c)
      (ε := 0)
      (a := 0)
      (b := T)
      hg.continuous.continuousOn
      (fun x _ r hr =>
        (hg x).hasDerivAt.hasDerivWithinAt.liminf_right_slope_le hr)
      le_rfl
      (fun x hx => by
        simpa using hbound x ⟨hx.1, le_of_lt hx.2⟩)
      t
      ht
  rw [gronwallBound_ε0, sub_zero] at hgronwall
  exact hgronwall

/-- A scalar energy/dissipation curve with an exact right-derivative identity.

`scale` records the coefficient in
`d/dt energy(t) = -scale * dissipation(t)`. The derivative is taken within
`[t, ∞)`, matching semigroups defined by nonnegative time increments. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem finiteEuclidean_langevinGenerator_basisDisplay
    {ι : Type*} [Fintype ι]
    (V f : EuclideanSpace ℝ ι → ℝ) (x : EuclideanSpace ℝ ι) :
    Laplacian.laplacian f x - inner ℝ (gradient V x) (gradient f x) =
      (∑ i, iteratedFDeriv ℝ 2 f x
        ![(EuclideanSpace.basisFun ι ℝ) i, (EuclideanSpace.basisFun ι ℝ) i]) -
        ∑ i, (gradient V x) i * (gradient f x) i := by
  have hlap_fun :
      Laplacian.laplacian f =
        fun x => ∑ i, iteratedFDeriv ℝ 2 f x
          ![(EuclideanSpace.basisFun ι ℝ) i, (EuclideanSpace.basisFun ι ℝ) i] :=
    InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis f
      (EuclideanSpace.basisFun ι ℝ)
  have hlap :
      Laplacian.laplacian f x =
        ∑ i, iteratedFDeriv ℝ 2 f x
          ![(EuclideanSpace.basisFun ι ℝ) i, (EuclideanSpace.basisFun ι ℝ) i] :=
    congrFun hlap_fun x
  have hinner :
      inner ℝ (gradient V x) (gradient f x) =
        ∑ i, (gradient V x) i * (gradient f x) i :=
    _root_.AutoSamplingTheory.TechnicalLemmas.Geometry.EuclideanSpaceCoordinates.euclideanSpace_inner_eq_sum_mul
      (gradient V x) (gradient f x)
  rw [hlap, hinner]

/-- Explicit coordinate-unit version of
`finiteEuclidean_langevinGenerator_basisDisplay`.

The additional `[DecidableEq ι]` instance is only used to unfold Mathlib's
`EuclideanSpace.basisFun` into `EuclideanSpace.single i 1`. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem finiteEuclidean_langevinGenerator_coordinateDisplay
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    (V f : EuclideanSpace ℝ ι → ℝ) (x : EuclideanSpace ℝ ι) :
    Laplacian.laplacian f x - inner ℝ (gradient V x) (gradient f x) =
      (∑ i, iteratedFDeriv ℝ 2 f x
        ![(EuclideanSpace.single i (1 : ℝ)), (EuclideanSpace.single i (1 : ℝ))]) -
        ∑ i, (gradient V x) i * (gradient f x) i := by
  simpa [EuclideanSpace.basisFun_apply] using
    finiteEuclidean_langevinGenerator_basisDisplay V f x

/-- Supplied-hypothesis finite-coordinate handoff from weighted-divergence
algebra to the Mathlib pointwise expression `Δ f - <∇V, ∇f>`.

The hypotheses still provide the coordinate product-rule output, the
Gibbs-weight chain-rule output, and the coordinate divergence sum.  This theorem
only replaces the coordinate second-derivative and gradient-product sums by
Mathlib's `Laplacian.laplacian` and `gradient` display. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem finiteEuclidean_expNeg_lineDeriv_fderiv_coordinateSum_langevinGenerator_display
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    {V f : EuclideanSpace ℝ ι → ℝ} {x : EuclideanSpace ℝ ι}
    (hV : DifferentiableAt ℝ V x)
    (hf : DifferentiableAt ℝ
      (fun y : EuclideanSpace ℝ ι => fderiv ℝ f y) x)
    (hgradF : ∀ i,
      fderiv ℝ f x (EuclideanSpace.single i (1 : ℝ)) = (gradient f x) i) :
    (∑ i, lineDeriv ℝ
        (fun y : EuclideanSpace ℝ ι =>
          Real.exp (-V y) * fderiv ℝ f y (EuclideanSpace.single i (1 : ℝ)))
        x (EuclideanSpace.single i (1 : ℝ))) =
      Real.exp (-V x) * (Laplacian.laplacian f x -
        inner ℝ (gradient V x) (gradient f x)) := by
  have hcoordLineDeriv : ∀ i,
      lineDeriv ℝ
        (fun y : EuclideanSpace ℝ ι =>
          Real.exp (-V y) * fderiv ℝ f y (EuclideanSpace.single i (1 : ℝ)))
        x (EuclideanSpace.single i (1 : ℝ)) =
        Real.exp (-V x) * iteratedFDeriv ℝ 2 f x
          ![(EuclideanSpace.single i (1 : ℝ)), (EuclideanSpace.single i (1 : ℝ))] +
        (gradient (fun y : EuclideanSpace ℝ ι => Real.exp (-V y)) x) i *
          (gradient f x) i := by
    intro i
    have hline :=
      _root_.AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.LineDeriv.lineDeriv_expNegPotential_mul_fderiv_coordinate_eq
        (V := V) (f := f) (x := x) i hV hf
    have hgradRho :=
      _root_.AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient.gradient_expNegPotential_coordinate_eq_of_differentiableAt
        (V := V) (x := x) hV i
    calc
      lineDeriv ℝ
          (fun y : EuclideanSpace ℝ ι =>
            Real.exp (-V y) * fderiv ℝ f y (EuclideanSpace.single i (1 : ℝ)))
          x (EuclideanSpace.single i (1 : ℝ)) =
        Real.exp (-V x) * iteratedFDeriv ℝ 2 f x
          ![(EuclideanSpace.single i (1 : ℝ)), (EuclideanSpace.single i (1 : ℝ))] -
        Real.exp (-V x) * (gradient V x) i *
          fderiv ℝ f x (EuclideanSpace.single i (1 : ℝ)) := by
        simpa only [EuclideanSpace.single, PiLp.single] using hline
      _ = Real.exp (-V x) * iteratedFDeriv ℝ 2 f x
          ![(EuclideanSpace.single i (1 : ℝ)), (EuclideanSpace.single i (1 : ℝ))] +
        (gradient (fun y : EuclideanSpace ℝ ι => Real.exp (-V y)) x) i *
          (gradient f x) i := by
        rw [hgradF i, hgradRho]
        ring
  exact finiteEuclidean_expNeg_weightedDivergence_langevinGenerator_coordinateHandoff
    (V := V) (f := f) (x := x)
    (divCoord := fun i => lineDeriv ℝ
        (fun y : EuclideanSpace ℝ ι =>
          Real.exp (-V y) * fderiv ℝ f y (EuclideanSpace.single i (1 : ℝ)))
        x (EuclideanSpace.single i (1 : ℝ)))
    hV rfl hcoordLineDeriv

/-- Coordinate-line-derivative sum display with the local gradient-coordinate
bridge discharged.

Compared with
`finiteEuclidean_expNeg_lineDeriv_fderiv_coordinateSum_langevinGenerator_display`,
this theorem removes the supplied hypothesis
`fderiv ℝ f x eᵢ = (gradient f x) i` using the pointwise
`fderiv`/`gradient` coordinate bridge from `DifferentiableAt ℝ f x`.

It is still only a pointwise finite-coordinate sum display.  It does not define
a divergence operator, assert that the sum is a divergence, prove integration
by parts, establish generator domains, or prove invariant Gibbs law,
reversibility, or KL/FI dissipation. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem finiteEuclidean_expNeg_lineDeriv_fderiv_coordinateSum_langevinGenerator_display_of_differentiableAt
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    {V f : EuclideanSpace ℝ ι → ℝ} {x : EuclideanSpace ℝ ι}
    (hV : DifferentiableAt ℝ V x)
    (hfderiv : DifferentiableAt ℝ
      (fun y : EuclideanSpace ℝ ι => fderiv ℝ f y) x)
    (hf : DifferentiableAt ℝ f x) :
    (∑ i, lineDeriv ℝ
        (fun y : EuclideanSpace ℝ ι =>
          Real.exp (-V y) * fderiv ℝ f y (EuclideanSpace.single i (1 : ℝ)))
        x (EuclideanSpace.single i (1 : ℝ))) =
      Real.exp (-V x) * (Laplacian.laplacian f x -
        inner ℝ (gradient V x) (gradient f x)) :=
  finiteEuclidean_expNeg_lineDeriv_fderiv_coordinateSum_langevinGenerator_display
    (V := V) (f := f) (x := x) hV hfderiv
    (fun i =>
      _root_.AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient.fderiv_apply_coordinate_eq_gradient_coordinate_of_differentiableAt
        (f := f) (x := x) i hf)

/-- Named coordinate-divergence version of the finite Euclidean Gibbs-weighted
first-derivative display.

The vector field is the coordinate representative
`y ↦ exp (-V y) * fderiv ℝ f y eᵢ`.  The theorem only rewrites the compiled
coordinate-sum display through the local pointwise `coordinateDivergence`
definition.  It does not identify this with any integration theorem, prove
weighted integration by parts, establish generator domains, or prove invariant
Gibbs law, reversibility, or KL/FI dissipation. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem weightedDivergence_gibbsWeight_langevinGenerator_algebra
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    {rho lapF divWeighted : ℝ} {gradRho gradV gradF : E}
    (hdiv : divWeighted = rho * lapF + inner ℝ gradRho gradF)
    (hgrad : gradRho = (-rho) • gradV) :
    divWeighted = rho * (lapF - inner ℝ gradV gradF) := by
  calc
    divWeighted = rho * lapF + inner ℝ gradRho gradF := hdiv
    _ = rho * lapF + inner ℝ ((-rho) • gradV) gradF := by rw [hgrad]
    _ = rho * lapF + (-rho) * inner ℝ gradV gradF := by
      simp [real_inner_smul_left]
    _ = rho * (lapF - inner ℝ gradV gradF) := by ring

/-- Source-facing specialization of
`weightedDivergence_gibbsWeight_langevinGenerator_algebra` with the Gibbs weight
`rho = exp (-Vx)`.  This is still only algebra after the product-rule and
chain-rule facts have been supplied. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem radialSmoothCutoff_hasCompactSupport [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {R : ℝ} (hR : 0 < R) :
    HasCompactSupport (radialSmoothCutoff R : E → ℝ) := by
  rw [hasCompactSupport_def]
  exact IsCompact.of_isClosed_subset
    (isCompact_closedBall (0 : E) (2 * R)) isClosed_closure
    (radialSmoothCutoff_tsupport_subset_closedBall hR)

/-- A single positive constant controls the second iterated Fréchet
derivative of every positive-scale radial cutoff by `C / R^2`.

The proof first bounds the second derivative of the unit-scale radial cutoff
using continuity and compact support.  It then writes the radius-`R` cutoff as
the unit cutoff composed with scalar dilation and applies Mathlib's exact
iterated-derivative composition rule for continuous linear maps. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem radialSmoothCutoff_tendsto_one (x : E) :
    Tendsto (fun R : ℝ => radialSmoothCutoff R x) atTop (𝓝 1) := by
  apply tendsto_atTop_of_eventually_const (i₀ := ‖x‖ + 1)
  intro R hR
  have hR_pos : 0 < R := by
    calc
      0 < ‖x‖ + 1 := by positivity
      _ ≤ R := hR
  apply radialSmoothCutoff_eq_one_of_norm_le hR_pos
  linarith

end Radial

section Plateau

/-- A compact subset of an open set admits a smooth compactly supported plateau in that set.

The function takes values in `[0, 1]` and is identically one on the compact set. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem tendsto_integral_norm_fderiv_radialSmoothCutoff_comp_toLp_apply
    {n : ℕ} {μ : Measure (Fin (n + 1) → ℝ)}
    {G : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ}
    (hG : Integrable G μ) :
    Tendsto
      (fun R : ℝ =>
        ∫ x, ‖fderiv ℝ
          (fun z => Cutoff.radialSmoothCutoff R
            (WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
          x (G x)‖ ∂μ)
      atTop (𝓝 0) := by
  let e : EuclideanSpace ℝ (Fin (n + 1)) ≃L[ℝ] (Fin (n + 1) → ℝ) :=
    PiLp.continuousLinearEquiv 2 ℝ (fun _ : Fin (n + 1) => ℝ)
  obtain ⟨C, hC_pos, hC⟩ :=
    Cutoff.radialSmoothCutoff_fderiv_bound
      (E := EuclideanSpace ℝ (Fin (n + 1)))
  let bound : (Fin (n + 1) → ℝ) → ℝ :=
    fun x => (C * ‖e.symm.toContinuousLinearMap‖) * ‖G x‖
  have hbound_integrable : Integrable bound μ := by
    exact (hG.norm.const_mul (C * ‖e.symm.toContinuousLinearMap‖))
  have hmeas :
      ∀ᶠ R : ℝ in atTop,
        AEStronglyMeasurable
          (fun x => ‖fderiv ℝ
            (fun z => Cutoff.radialSmoothCutoff R
              (WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
            x (G x)‖) μ := by
    filter_upwards [eventually_gt_atTop (0 : ℝ)] with R hR
    have hsmooth :
        ContDiff ℝ (⊤ : ℕ∞)
          (fun z : Fin (n + 1) → ℝ =>
            Cutoff.radialSmoothCutoff R
              (WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1)))) :=
      (Cutoff.radialSmoothCutoff_contDiff hR).comp
        (PiLp.contDiff_toLp (𝕜 := ℝ) (E := fun _ : Fin (n + 1) => ℝ))
    have hderiv :
        AEStronglyMeasurable
          (fun x => fderiv ℝ
            (fun z : Fin (n + 1) → ℝ =>
              Cutoff.radialSmoothCutoff R
                (WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
            x) μ :=
      (hsmooth.continuous_fderiv
        (WithTop.coe_ne_zero.mpr WithTop.top_ne_zero)).aestronglyMeasurable
    let eval :
        ((Fin (n + 1) → ℝ) →L[ℝ] ℝ) →L[ℝ]
          (Fin (n + 1) → ℝ) →L[ℝ] ℝ :=
      ContinuousLinearMap.flip (ContinuousLinearMap.apply ℝ ℝ)
    exact
      (eval.aestronglyMeasurable_comp₂
        hderiv hG.aestronglyMeasurable).norm
  have hdom :
      ∀ᶠ R : ℝ in atTop, ∀ᵐ x ∂μ,
        ‖(fun x => ‖fderiv ℝ
          (fun z => Cutoff.radialSmoothCutoff R
            (WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
          x (G x)‖) x‖ ≤ bound x := by
    filter_upwards [eventually_ge_atTop (1 : ℝ)] with R hR
    filter_upwards with x
    have hR_pos : 0 < R := lt_of_lt_of_le zero_lt_one hR
    have hfderiv :
        fderiv ℝ
          (fun z => Cutoff.radialSmoothCutoff R
            (WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
          x =
        (fderiv ℝ
          (Cutoff.radialSmoothCutoff R :
            EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
          (WithLp.toLp 2 x)).comp e.symm.toContinuousLinearMap :=
      (hasFDerivAt_radialSmoothCutoff_comp_toLp hR_pos x).fderiv
    rw [norm_norm, hfderiv]
    calc
      ‖((fderiv ℝ
          (Cutoff.radialSmoothCutoff R :
            EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
          (WithLp.toLp 2 x)).comp e.symm.toContinuousLinearMap) (G x)‖
          ≤ ‖(fderiv ℝ
              (Cutoff.radialSmoothCutoff R :
                EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
              (WithLp.toLp 2 x)).comp e.symm.toContinuousLinearMap‖ * ‖G x‖ :=
        ContinuousLinearMap.le_opNorm _ _
      _ ≤ ((C / R) * ‖e.symm.toContinuousLinearMap‖) * ‖G x‖ := by
        gcongr
        exact (ContinuousLinearMap.opNorm_comp_le _ _).trans
          (mul_le_mul_of_nonneg_right
            (hC R hR_pos (WithLp.toLp 2 x)) (norm_nonneg _))
      _ ≤ bound x := by
        dsimp [bound]
        gcongr
        exact div_le_self hC_pos.le hR
  have hpoint :
      ∀ᵐ x ∂μ,
        Tendsto
          (fun R : ℝ => ‖fderiv ℝ
            (fun z => Cutoff.radialSmoothCutoff R
              (WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
            x (G x)‖)
          atTop (𝓝 0) := by
    filter_upwards with x
    refine squeeze_zero'
      (g := fun R =>
        ((C / R) * ‖e.symm.toContinuousLinearMap‖) * ‖G x‖) ?_ ?_ ?_
    · exact Filter.Eventually.of_forall fun R => norm_nonneg _
    · filter_upwards [eventually_gt_atTop (0 : ℝ)] with R hR
      have hfderiv :
          fderiv ℝ
            (fun z => Cutoff.radialSmoothCutoff R
              (WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
            x =
          (fderiv ℝ
            (Cutoff.radialSmoothCutoff R :
              EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
            (WithLp.toLp 2 x)).comp e.symm.toContinuousLinearMap :=
        (hasFDerivAt_radialSmoothCutoff_comp_toLp hR x).fderiv
      rw [hfderiv]
      calc
        ‖((fderiv ℝ
            (Cutoff.radialSmoothCutoff R :
              EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
            (WithLp.toLp 2 x)).comp e.symm.toContinuousLinearMap) (G x)‖
            ≤ ‖(fderiv ℝ
                  (Cutoff.radialSmoothCutoff R :
                    EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
                  (WithLp.toLp 2 x)).comp e.symm.toContinuousLinearMap‖ *
                  ‖G x‖ := ContinuousLinearMap.le_opNorm _ _
        _ ≤ ((C / R) * ‖e.symm.toContinuousLinearMap‖) * ‖G x‖ := by
          gcongr
          exact (ContinuousLinearMap.opNorm_comp_le _ _).trans
            (mul_le_mul_of_nonneg_right
              (hC R hR (WithLp.toLp 2 x)) (norm_nonneg _))
    · simpa [mul_assoc] using
        (tendsto_const_nhds.div_atTop tendsto_id).mul_const
          (‖e.symm.toContinuousLinearMap‖ * ‖G x‖)
  have hDCT :=
    MeasureTheory.tendsto_integral_filter_of_dominated_convergence
      (μ := μ) (l := atTop)
      (F := fun R x => ‖fderiv ℝ
        (fun z => Cutoff.radialSmoothCutoff R
          (WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
        x (G x)‖)
      (f := fun _ => (0 : ℝ)) bound hmeas hdom hbound_integrable hpoint
  simpa using hDCT

/-- Multiplication by the PiLp-wrapped radial cutoff converges to the identity
under integration for every integrable real normed-space-valued source field.

The statement is measure-generic and uses only integrability of the source.
It proves the cutoff main-term limit, but no Gibbs-specific integrability,
cutoff-gradient estimate, integration by parts, generator-domain result, or
invariant-law statement. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem tendsto_integral_radialSmoothCutoff_comp_toLp_smul
    {n : ℕ} {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
    {μ : Measure (Fin (n + 1) → ℝ)}
    {H : (Fin (n + 1) → ℝ) → F}
    (hH : Integrable H μ) :
    Tendsto
      (fun R : ℝ => ∫ x,
        Cutoff.radialSmoothCutoff R
          (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) • H x ∂μ)
      atTop (𝓝 (∫ x, H x ∂μ)) := by
  have hmeas :
      ∀ᶠ R : ℝ in atTop,
        AEStronglyMeasurable
          (fun x : Fin (n + 1) → ℝ =>
            Cutoff.radialSmoothCutoff R
              (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) • H x) μ := by
    filter_upwards [eventually_gt_atTop (0 : ℝ)] with R hR
    exact
      (((Cutoff.radialSmoothCutoff_contDiff hR).continuous.comp
        (PiLp.continuous_toLp 2 _)).aestronglyMeasurable).smul
        hH.aestronglyMeasurable
  have hdom :
      ∀ᶠ R : ℝ in atTop, ∀ᵐ x ∂μ,
        ‖Cutoff.radialSmoothCutoff R
            (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) • H x‖ ≤
          ‖H x‖ := by
    filter_upwards with R
    filter_upwards with x
    have hcutoff :=
      Cutoff.radialSmoothCutoff_mem_Icc R
        (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1)))
    rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg hcutoff.1]
    exact mul_le_of_le_one_left (norm_nonneg _) hcutoff.2
  have hpoint :
      ∀ᵐ x ∂μ,
        Tendsto
          (fun R : ℝ =>
            Cutoff.radialSmoothCutoff R
              (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) • H x)
          atTop (𝓝 (H x)) := by
    filter_upwards with x
    simpa using
      (Cutoff.radialSmoothCutoff_tendsto_one
        (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1)))).smul_const (H x)
  exact MeasureTheory.tendsto_integral_filter_of_dominated_convergence
    (μ := μ) (l := atTop)
    (F := fun R x =>
      Cutoff.radialSmoothCutoff R
        (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) • H x)
    (f := H) (fun x => ‖H x‖) hmeas hdom hH.norm hpoint

/-- The `L¹` norm of an integrable field on the complement of an expanding
Euclidean ball tends to zero, expressed in raw finite-Pi coordinates.

The tail sets are `R ≤ ‖WithLp.toLp 2 x‖`.  They form an antitone family with
empty intersection, so Mathlib's antitone set-integral convergence theorem
applies to `‖H‖`.  This is measure-generic and contains no Gibbs, generator,
integration-by-parts, or invariance semantics. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem integral_expNeg_langevinGenerator_rhs_eq_zero_of_contDiff_of_hasCompactSupport
    {n : ℕ}
    {V f : EuclideanSpace ℝ (Fin (n + 1)) → ℝ}
    (hV : ContDiff ℝ 1 V)
    (hf : ContDiff ℝ 2 f)
    (hf_support : HasCompactSupport f) :
    ∫ y : EuclideanSpace ℝ (Fin (n + 1)),
        Real.exp (-V y) *
          (Laplacian.laplacian f y - inner ℝ (gradient V y) (gradient f y)) = 0 := by
  let e : EuclideanSpace ℝ (Fin (n + 1)) ≃L[ℝ] (Fin (n + 1) → ℝ) :=
    PiLp.continuousLinearEquiv 2 ℝ (fun _ : Fin (n + 1) => ℝ)
  let F : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ :=
    fun z => fun i =>
      Real.exp (-V (e.symm z)) *
        fderiv ℝ f (e.symm z) (EuclideanSpace.single i (1 : ℝ))
  have hF : ContDiff ℝ 1 F := by
    apply contDiff_pi.2
    intro i
    exact (hV.comp e.symm.contDiff).neg.exp.mul
      (((hf.fderiv_right (m := 1) (by norm_num)).comp e.symm.contDiff).clm_apply
        contDiff_const)
  have hF_support : HasCompactSupport F := by
    refine HasCompactSupport.of_support_subset_isCompact
      (hf_support.isCompact.image e.continuous) ?_
    intro x hx
    have hxe : e.symm x ∈ tsupport f := by
      by_contra hxe
      have hzero : fderiv ℝ f (e.symm x) = 0 :=
        fderiv_of_notMem_tsupport ℝ hxe
      exact hx (by
        funext i
        simp [F, hzero])
    exact ⟨e.symm x, hxe, e.apply_symm_apply x⟩
  have hdiv :=
    _root_.AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.integral_coordinateDivergence_wrapped_eq_zero_of_contDiff_of_hasCompactSupport
      F hF hF_support
  have hraw :
      ∫ x : Fin (n + 1) → ℝ,
          Real.exp (-V (e.symm x)) *
            (Laplacian.laplacian f (e.symm x) -
              inner ℝ (gradient V (e.symm x)) (gradient f (e.symm x))) = 0 := by
    calc
      ∫ x : Fin (n + 1) → ℝ,
          Real.exp (-V (e.symm x)) *
            (Laplacian.laplacian f (e.symm x) -
              inner ℝ (gradient V (e.symm x)) (gradient f (e.symm x))) =
          ∫ x : Fin (n + 1) → ℝ,
            _root_.AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.coordinateDivergence
              (fun y : EuclideanSpace ℝ (Fin (n + 1)) =>
                (WithLp.toLp 2 (F (WithLp.ofLp y)) :
                  EuclideanSpace ℝ (Fin (n + 1))))
              (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) := by
        apply integral_congr_ae
        exact Filter.Eventually.of_forall fun x => by
          have htrace :=
            trace_expNeg_fderivCoordinateField_langevinGenerator_display_of_hasFDerivAt
              (V := V) (f := f) (x := x) (F' := fderiv ℝ F x)
              (by simpa [F, e] using (hF.differentiable one_ne_zero x).hasFDerivAt)
              (hV.differentiable one_ne_zero _)
              ((hf.fderiv_right (m := 1) (by norm_num)).differentiable one_ne_zero _)
              (hf.differentiable (by norm_num) _)
          have hwrapped :=
            _root_.AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.coordinateDivergence_wrapped_toPi_trace_of_hasFDerivAt
              (ι := Fin (n + 1)) (hF.differentiable one_ne_zero x).hasFDerivAt
          change
            Real.exp (-V (e.symm x)) *
                (Laplacian.laplacian f (e.symm x) -
                  inner ℝ (gradient V (e.symm x)) (gradient f (e.symm x))) =
              _root_.AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.coordinateDivergence
                (fun y : EuclideanSpace ℝ (Fin (n + 1)) =>
                  (WithLp.toLp 2 (F (WithLp.ofLp y)) :
                    EuclideanSpace ℝ (Fin (n + 1))))
                (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1)))
          calc
            _ = ∑ i, fderiv ℝ F x (Pi.single i (1 : ℝ)) i := by
              simpa [e] using htrace.symm
            _ = _ := hwrapped.symm
      _ = 0 := by simpa [F, e] using hdiv
  rw [← (PiLp.volume_preserving_toLp (Fin (n + 1))).integral_comp
    (MeasurableEquiv.toLp 2 _).measurableEmbedding]
  simpa [e] using hraw

/-- Whole-space integrability of the Gibbs-weighted coordinate derivative
field from finiteness of the unnormalized Gibbs mass and a uniform operator
norm bound on the test-function derivative.

This theorem proves only source-field integrability.  It does not prove a
cutoff main-term limit, weighted integration by parts, stationarity, or an
invariant Gibbs law. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem isProbabilityMeasure_withDensity_normalized_gibbs
    (μ : MeasureTheory.Measure α) (V : α → ℝ)
    (h0 : ∫⁻ x, gibbsDensityENNReal V x ∂μ ≠ 0)
    (hfin : ∫⁻ x, gibbsDensityENNReal V x ∂μ ≠ ∞) :
    IsProbabilityMeasure
      (μ.withDensity fun x =>
        (∫⁻ y, gibbsDensityENNReal V y ∂μ)⁻¹ * gibbsDensityENNReal V x) :=
  RadonNikodym.isProbabilityMeasure_withDensity_normalized_lintegral μ
    (gibbsDensityENNReal V) h0 hfin

/-- A nonzero base measure and a finite a.e. envelope are enough to normalize a
Gibbs density into a probability measure.  This is the reusable contract that
later coercivity/growth leaves should target. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem integral_operator_normalizedGibbs_eq_zero_on_compactlySupportedC2
    {n : ℕ}
    {V f : EuclideanSpace ℝ (Fin (n + 1)) → ℝ}
    (hV : ContDiff ℝ 1 V)
    (hf : CompactlySupportedC2 f) :
    ∫ x, operator V f x ∂volume.withDensity
        (fun x =>
          (∫⁻ y, Measure.Gibbs.gibbsDensityENNReal V y ∂volume)⁻¹ *
            Measure.Gibbs.gibbsDensityENNReal V x) = 0 := by
  rw [TechnicalLemmas.Measure.GibbsIntegral.integral_withDensity_lintegral_inv_mul_gibbsDensityENNReal_eq_integral_lintegral_inv_mul_exp_smul_of_neZero
    volume hV.continuous.measurable.aemeasurable]
  simp_rw [operator, smul_eq_mul, mul_assoc]
  rw [integral_const_mul]
  rw [Langevin.integral_expNeg_langevinGenerator_rhs_eq_zero_of_contDiff_of_hasCompactSupport
    hV hf.1 hf.2]
  simp

/-- A semigroup satisfying the integrated-generator contract on the
compactly supported `C²` core preserves normalized Gibbs expectations on that
core.

This theorem composes the concrete Gibbs integration-by-parts identity with
the abstract semigroup-to-invariance bridge.  The semigroup contract remains
an explicit hypothesis: no Langevin SDE, Markov semigroup, core closure, or
measure-determining extension is constructed here. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem isInvariantOn_normalizedGibbs_on_compactlySupportedC2
    {n : ℕ}
    {V : EuclideanSpace ℝ (Fin (n + 1)) → ℝ}
    {P : ℝ →
      (EuclideanSpace ℝ (Fin (n + 1)) → ℝ) →
        EuclideanSpace ℝ (Fin (n + 1)) → ℝ}
    {generator :
      (EuclideanSpace ℝ (Fin (n + 1)) → ℝ) →
        EuclideanSpace ℝ (Fin (n + 1)) → ℝ}
    (hV : ContDiff ℝ 1 V)
    (hcore : CoreContract V generator (Set.ofPred CompactlySupportedC2))
    (hsemigroup : WeakGenerator.IntegratedSemigroupGeneratorContract
      P generator (Set.ofPred CompactlySupportedC2)
      (volume.withDensity
        (fun x =>
          (∫⁻ y, Measure.Gibbs.gibbsDensityENNReal V y ∂volume)⁻¹ *
            Measure.Gibbs.gibbsDensityENNReal V x))) :
    WeakGenerator.IsInvariantOn P
      (volume.withDensity
        (fun x =>
          (∫⁻ y, Measure.Gibbs.gibbsDensityENNReal V y ∂volume)⁻¹ *
            Measure.Gibbs.gibbsDensityENNReal V x))
      (Set.ofPred CompactlySupportedC2) := by
  refine WeakGenerator.isInvariantOn_of_integral_generator_eq_zero hsemigroup ?_
  intro f hf
  rw [hcore.generator_eq_operator_on_core f hf]
  exact integral_operator_normalizedGibbs_eq_zero_on_compactlySupportedC2 hV hf

end LangevinGenerator
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

noncomputable def variance (μ : Measure E) (f : E → ℝ) : ℝ :=
  ∫ x, (f x - ∫ y, f y ∂μ) ^ 2 ∂μ

/-- The Euclidean/inner-product Dirichlet energy of a test function. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

noncomputable def dirichletEnergy (μ : Measure E) (f : E → ℝ) : ℝ :=
  ∫ x, ‖gradient f x‖ ^ 2 ∂μ

/-- Exact integrability domain used by the local Poincare interface. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

def Admissible (μ : Measure E) (f : E → ℝ) : Prop :=
  Integrable f μ ∧
    Integrable (fun x => (f x - ∫ y, f y ∂μ) ^ 2) μ ∧
    Integrable (fun x => ‖gradient f x‖ ^ 2) μ

/-- A measure satisfies the Poincare inequality with constant `C` on an
explicit test class.

The convention is `Var_μ(f) ≤ C * E_μ(f)`.  Probability normalization is
part of the contract rather than an implicit convention. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

def Satisfies (μ : Measure E) (tests : Set (E → ℝ)) (C : ℝ) : Prop :=
  IsProbabilityMeasure μ ∧ 0 ≤ C ∧
    ∀ f ∈ tests, Admissible μ f → variance μ f ≤ C * dirichletEnergy μ f

omit [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] in
/-- Variance is nonnegative on its stated integral representation. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem variance_nonneg {μ : Measure E} {f : E → ℝ} :
    0 ≤ variance μ f := by
  rw [variance]
  exact integral_nonneg_of_ae
    (Filter.Eventually.of_forall fun x => sq_nonneg (f x - ∫ y, f y ∂μ))

/-- Dirichlet energy is nonnegative on its stated integrability domain. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem dirichletEnergy_nonneg {μ : Measure E} {f : E → ℝ} :
    0 ≤ dirichletEnergy μ f := by
  rw [dirichletEnergy]
  exact integral_nonneg_of_ae
    (Filter.Eventually.of_forall fun x => sq_nonneg ‖gradient f x‖)

/-- Increasing a nonnegative Poincare constant preserves the inequality on
the same test class and admissibility domain. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem mono_constant {μ : Measure E} {tests : Set (E → ℝ)} {C D : ℝ}
    (hC : Satisfies μ tests C) (hCD : C ≤ D) :
    Satisfies μ tests D := by
  refine ⟨hC.1, hC.2.1.trans hCD, ?_⟩
  intro f hf_tests hf
  exact (hC.2.2 f hf_tests hf).trans
    (mul_le_mul_of_nonneg_right hCD dirichletEnergy_nonneg)

/-- The inequality component can be consumed without unpacking the probability
and nonnegative-constant fields manually. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem variance_le {μ : Measure E} {tests : Set (E → ℝ)} {C : ℝ}
    (hC : Satisfies μ tests C) {f : E → ℝ}
    (hf_tests : f ∈ tests) (hf : Admissible μ f) :
    variance μ f ≤ C * dirichletEnergy μ f :=
  hC.2.2 f hf_tests hf

/-- Restricting the test class preserves a Poincare inequality and all of its
measure and constant data. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem mono_tests {μ : Measure E} {small large : Set (E → ℝ)} {C : ℝ}
    (hC : Satisfies μ large C) (hsub : small ⊆ large) :
    Satisfies μ small C := by
  refine ⟨hC.1, hC.2.1, ?_⟩
  intro f hf_tests
  exact hC.2.2 f (hsub hf_tests)

end Poincare
end FunctionalInequalities
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem exponential_decay_of_scaled_dissipation
    {scale rate : ℝ} (curve : DissipationCurve scale)
    (hcoercive : ∀ s : ℝ,
      rate * curve.energy s ≤ scale * curve.dissipation s)
    {t : ℝ} (ht : 0 ≤ t) :
    curve.energy t ≤ curve.energy 0 * Real.exp (-rate * t) := by
  simpa [sub_zero] using
    exponential_decay_of_scaled_dissipation_from
      curve hcoercive ht

/-- Exponential decay from every starting time forces the instantaneous
coercivity inequality.

The proof compares the energy with its exponential envelope on `[s, ∞)`. Their
difference has a local maximum at `s`; the one-sided Fermat inequality then
compares the two right derivatives. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem chewi_theorem_1_2_21_forward
    {C : ℝ} (hC : 0 < C) (curve : DissipationCurve 2)
    (hPI : ∀ s : ℝ,
      curve.energy s ≤ C * curve.dissipation s)
    {t : ℝ} (ht : 0 ≤ t) :
    curve.energy t ≤
      curve.energy 0 * Real.exp (-(2 / C) * t) := by
  simpa [sub_zero] using
    chewi_theorem_1_2_21_forward_from hC curve hPI ht

/-- Backward scalar direction of Chewi, Theorem 1.2.21. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem chewi_theorem_1_2_22_forward
    {C : ℝ} (hC : 0 < C) (curve : DissipationCurve 2)
    (hPI : ∀ s : ℝ,
      curve.energy s ≤ C * curve.dissipation s)
    {t : ℝ} (ht : 0 ≤ t) :
    curve.energy t ≤
      curve.energy 0 * Real.exp (-(2 / C) * t) :=
  chewi_theorem_1_2_21_forward hC curve hPI ht

/-- Backward scalar direction of Chewi, Theorem 1.2.22. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem exponential_decay_of_scaled_dissipation_from
    {scale rate : ℝ} (curve : DissipationCurve scale)
    (hcoercive : ∀ u : ℝ,
      rate * curve.energy u ≤ scale * curve.dissipation u)
    {s t : ℝ} (hst : s ≤ t) :
    curve.energy t ≤
      curve.energy s * Real.exp (-rate * (t - s)) := by
  have hbound : ∀ x ∈ Ico s t,
      -scale * curve.dissipation x ≤
        (-rate) * curve.energy x + 0 := by
    intro x hx
    have hneg := neg_le_neg (hcoercive x)
    simpa [neg_mul] using hneg
  have hgronwall :=
    le_gronwallBound_of_liminf_deriv_right_le
      (f := curve.energy)
      (f' := fun x => -scale * curve.dissipation x)
      (δ := curve.energy s)
      (K := -rate)
      (ε := 0)
      (a := s)
      (b := t)
      curve.energy_continuous.continuousOn
      (fun x hx r hr => by
        simpa [slope] using
          (curve.energy_hasDerivWithinAt x).liminf_right_slope_le hr)
      le_rfl
      hbound
      t
      ⟨hst, le_rfl⟩
  rw [gronwallBound_ε0] at hgronwall
  exact hgronwall

/-- A coercive inequality along a dissipation curve implies exponential decay
from time zero. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem scaled_dissipation_of_exponential_decay
    {scale rate : ℝ} (curve : DissipationCurve scale)
    (hdecay : ∀ s t : ℝ, 0 ≤ t →
      curve.energy (s + t) ≤
        curve.energy s * Real.exp (-rate * t)) :
    ∀ s : ℝ,
      rate * curve.energy s ≤ scale * curve.dissipation s := by
  intro s
  let comparison : ℝ → ℝ := fun x =>
    curve.energy x -
      curve.energy s * Real.exp (-rate * (x - s))
  have hmax : IsLocalMaxOn comparison (Ici s) s := by
    filter_upwards [self_mem_nhdsWithin] with x hx
    have hdecay_x :
        curve.energy x ≤
          curve.energy s * Real.exp (-rate * (x - s)) := by
      have h := hdecay s (x - s) (sub_nonneg.mpr hx)
      calc
        curve.energy x = curve.energy (s + (x - s)) := by
          congr 1
          ring
        _ ≤ curve.energy s * Real.exp (-rate * (x - s)) := h
    dsimp [comparison]
    calc
      curve.energy x -
          curve.energy s * Real.exp (-rate * (x - s)) ≤ 0 :=
        sub_nonpos.mpr hdecay_x
      _ = curve.energy s -
          curve.energy s * Real.exp (-rate * (s - s)) := by simp
  have hinner :
      HasDerivAt (fun x : ℝ => -rate * (x - s)) (-rate) s := by
    change HasDerivAt (fun y : ℝ => -rate * (id y - s)) (-rate) s
    have hraw := ((hasDerivAt_id s).sub_const s).const_mul (-rate)
    exact hraw.congr_deriv (by ring)
  have hexponential :
      HasDerivAt
        (fun x : ℝ =>
          curve.energy s * Real.exp (-rate * (x - s)))
        (-rate * curve.energy s) s := by
    have hraw := hinner.exp.const_mul (curve.energy s)
    apply hraw.congr_deriv
    rw [sub_self, mul_zero, Real.exp_zero]
    ring
  have hderiv :
      HasDerivWithinAt comparison
        ((-scale * curve.dissipation s) -
          (-rate * curve.energy s))
        (Ici s) s := by
    change HasDerivWithinAt
      (curve.energy - fun x : ℝ =>
        curve.energy s * Real.exp (-rate * (x - s)))
      ((-scale * curve.dissipation s) - (-rate * curve.energy s))
      (Ici s) s
    exact (curve.energy_hasDerivWithinAt s).sub
      hexponential.hasDerivWithinAt
  have hone : (1 : ℝ) ∈ posTangentConeAt (Ici s) s := by
    rw [one_mem_posTangentConeAt_iff_frequently]
    have hev : ∀ᶠ x in 𝓝[>] s, x ∈ Ici s := by
      filter_upwards [self_mem_nhdsWithin] with x hx
      have hsx : s < x := by
        simpa only [mem_Ioi] using hx
      exact hsx.le
    exact hev.frequently
  have hnonpos :=
    hmax.hasFDerivWithinAt_nonpos hderiv.hasFDerivWithinAt hone
  have hscalar :
      ((-scale * curve.dissipation s) -
        (-rate * curve.energy s)) ≤ 0 := by
    simpa using hnonpos
  linarith

/-- Forward direction of Chewi, Theorem 1.2.21, between arbitrary times. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem chewi_theorem_1_2_21_scalar_equivalence
    {C : ℝ} (hC : 0 < C) (curve : DissipationCurve 2) :
    (∀ s : ℝ,
      curve.energy s ≤ C * curve.dissipation s) ↔
    (∀ s t : ℝ, 0 ≤ t →
      curve.energy (s + t) ≤
        curve.energy s * Real.exp (-(2 / C) * t)) := by
  constructor
  · intro hPI s t ht
    have h := chewi_theorem_1_2_21_forward_from
      hC curve hPI (show s ≤ s + t by linarith)
    simpa using h
  · exact chewi_theorem_1_2_21_backward hC curve

/-- Forward direction of Chewi, Theorem 1.2.22, between arbitrary times. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem chewi_theorem_1_2_22_scalar_equivalence
    {C : ℝ} (hC : 0 < C) (curve : DissipationCurve 2) :
    (∀ s : ℝ,
      curve.energy s ≤ C * curve.dissipation s) ↔
    (∀ s t : ℝ, 0 ≤ t →
      curve.energy (s + t) ≤
        curve.energy s * Real.exp (-(2 / C) * t)) :=
  chewi_theorem_1_2_21_scalar_equivalence hC curve

/-- Forward direction of Chewi, Theorem 1.2.26, between arbitrary times. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

def Satisfies (μ : Measure E) (tests : Set (E → ℝ)) (C : ℝ) : Prop :=
  IsProbabilityMeasure μ ∧ 0 ≤ C ∧
    ∀ f ∈ tests, Admissible μ f → variance μ f ≤ C * dirichletEnergy μ f

omit [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] in
/-- Variance is nonnegative on its stated integral representation. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem mono_constant {μ : Measure E} {tests : Set (E → ℝ)} {C D : ℝ}
    (hC : Satisfies μ tests C) (hCD : C ≤ D) :
    Satisfies μ tests D := by
  refine ⟨hC.1, hC.2.1.trans hCD, ?_⟩
  intro f hf_tests hf
  exact (hC.2.2 f hf_tests hf).trans
    (mul_le_mul_of_nonneg_right hCD dirichletEnergy_nonneg)

/-- The inequality component can be consumed without unpacking the probability
and nonnegative-constant fields manually. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem mono_tests {μ : Measure E} {small large : Set (E → ℝ)} {C : ℝ}
    (hC : Satisfies μ large C) (hsub : small ⊆ large) :
    Satisfies μ small C := by
  refine ⟨hC.1, hC.2.1, ?_⟩
  intro f hf_tests
  exact hC.2.2 f (hsub hf_tests)

end Poincare
end FunctionalInequalities
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem lsiKlFiSqrtDensityFisherChainIntegralHandoffScalar
    {α ι : Type*} [MeasurableSpace α] [Fintype ι] (mu : Measure α)
    {r : α → Real} {dirichlet fisher : Real} {dr dSqrt dLog : ι → α → Real}
    (hdirichlet : dirichlet = ∫ x, (∑ i, dSqrt i x ^ 2) ∂mu)
    (hfisher : fisher = ∫ x, (r x * ∑ i, dLog i x ^ 2) ∂mu)
    (hr : ∀ᵐ x ∂mu, 0 < r x)
    (hdSqrt : ∀ᵐ x ∂mu,
      ∀ i, dSqrt i x = (1 / (2 * Real.sqrt (r x))) * dr i x)
    (hdLog : ∀ᵐ x ∂mu, ∀ i, dLog i x = dr i x / r x) :
    dirichlet = (1 / 4) * fisher := by
  rw [hdirichlet, hfisher]
  rw [← integral_const_mul]
  exact lsiKlFiSqrtDensityFisherChainIntegralFiniteSum mu hr hdSqrt hdLog

/-- Scalar rearrangement behind the one-sided use of the cited DV formula.

This is not a proof of Donsker--Varadhan.  It starts after a cited or
eventually formalized entropy-duality theorem has supplied the variational
upper bound for an admissible test.
-/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem exponential_decay_of_scaled_dissipation
    {scale rate : ℝ} (curve : DissipationCurve scale)
    (hcoercive : ∀ s : ℝ,
      rate * curve.energy s ≤ scale * curve.dissipation s)
    {t : ℝ} (ht : 0 ≤ t) :
    curve.energy t ≤ curve.energy 0 * Real.exp (-rate * t) := by
  simpa [sub_zero] using
    exponential_decay_of_scaled_dissipation_from
      curve hcoercive ht

/-- Exponential decay from every starting time forces the instantaneous
coercivity inequality.

The proof compares the energy with its exponential envelope on `[s, ∞)`. Their
difference has a local maximum at `s`; the one-sided Fermat inequality then
compares the two right derivatives. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem chewi_theorem_1_2_26_forward
    {C : ℝ} (hC : 0 < C) (curve : DissipationCurve 1)
    (hLSI : ∀ s : ℝ,
      curve.energy s ≤ (C / 2) * curve.dissipation s)
    {t : ℝ} (ht : 0 ≤ t) :
    curve.energy t ≤
      curve.energy 0 * Real.exp (-(2 / C) * t) := by
  simpa [sub_zero] using
    chewi_theorem_1_2_26_forward_from hC curve hLSI ht

/-- Backward scalar direction of Chewi, Theorem 1.2.26. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem exponential_decay_of_scaled_dissipation_from
    {scale rate : ℝ} (curve : DissipationCurve scale)
    (hcoercive : ∀ u : ℝ,
      rate * curve.energy u ≤ scale * curve.dissipation u)
    {s t : ℝ} (hst : s ≤ t) :
    curve.energy t ≤
      curve.energy s * Real.exp (-rate * (t - s)) := by
  have hbound : ∀ x ∈ Ico s t,
      -scale * curve.dissipation x ≤
        (-rate) * curve.energy x + 0 := by
    intro x hx
    have hneg := neg_le_neg (hcoercive x)
    simpa [neg_mul] using hneg
  have hgronwall :=
    le_gronwallBound_of_liminf_deriv_right_le
      (f := curve.energy)
      (f' := fun x => -scale * curve.dissipation x)
      (δ := curve.energy s)
      (K := -rate)
      (ε := 0)
      (a := s)
      (b := t)
      curve.energy_continuous.continuousOn
      (fun x hx r hr => by
        simpa [slope] using
          (curve.energy_hasDerivWithinAt x).liminf_right_slope_le hr)
      le_rfl
      hbound
      t
      ⟨hst, le_rfl⟩
  rw [gronwallBound_ε0] at hgronwall
  exact hgronwall

/-- A coercive inequality along a dissipation curve implies exponential decay
from time zero. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem scaled_dissipation_of_exponential_decay
    {scale rate : ℝ} (curve : DissipationCurve scale)
    (hdecay : ∀ s t : ℝ, 0 ≤ t →
      curve.energy (s + t) ≤
        curve.energy s * Real.exp (-rate * t)) :
    ∀ s : ℝ,
      rate * curve.energy s ≤ scale * curve.dissipation s := by
  intro s
  let comparison : ℝ → ℝ := fun x =>
    curve.energy x -
      curve.energy s * Real.exp (-rate * (x - s))
  have hmax : IsLocalMaxOn comparison (Ici s) s := by
    filter_upwards [self_mem_nhdsWithin] with x hx
    have hdecay_x :
        curve.energy x ≤
          curve.energy s * Real.exp (-rate * (x - s)) := by
      have h := hdecay s (x - s) (sub_nonneg.mpr hx)
      calc
        curve.energy x = curve.energy (s + (x - s)) := by
          congr 1
          ring
        _ ≤ curve.energy s * Real.exp (-rate * (x - s)) := h
    dsimp [comparison]
    calc
      curve.energy x -
          curve.energy s * Real.exp (-rate * (x - s)) ≤ 0 :=
        sub_nonpos.mpr hdecay_x
      _ = curve.energy s -
          curve.energy s * Real.exp (-rate * (s - s)) := by simp
  have hinner :
      HasDerivAt (fun x : ℝ => -rate * (x - s)) (-rate) s := by
    change HasDerivAt (fun y : ℝ => -rate * (id y - s)) (-rate) s
    have hraw := ((hasDerivAt_id s).sub_const s).const_mul (-rate)
    exact hraw.congr_deriv (by ring)
  have hexponential :
      HasDerivAt
        (fun x : ℝ =>
          curve.energy s * Real.exp (-rate * (x - s)))
        (-rate * curve.energy s) s := by
    have hraw := hinner.exp.const_mul (curve.energy s)
    apply hraw.congr_deriv
    rw [sub_self, mul_zero, Real.exp_zero]
    ring
  have hderiv :
      HasDerivWithinAt comparison
        ((-scale * curve.dissipation s) -
          (-rate * curve.energy s))
        (Ici s) s := by
    change HasDerivWithinAt
      (curve.energy - fun x : ℝ =>
        curve.energy s * Real.exp (-rate * (x - s)))
      ((-scale * curve.dissipation s) - (-rate * curve.energy s))
      (Ici s) s
    exact (curve.energy_hasDerivWithinAt s).sub
      hexponential.hasDerivWithinAt
  have hone : (1 : ℝ) ∈ posTangentConeAt (Ici s) s := by
    rw [one_mem_posTangentConeAt_iff_frequently]
    have hev : ∀ᶠ x in 𝓝[>] s, x ∈ Ici s := by
      filter_upwards [self_mem_nhdsWithin] with x hx
      have hsx : s < x := by
        simpa only [mem_Ioi] using hx
      exact hsx.le
    exact hev.frequently
  have hnonpos :=
    hmax.hasFDerivWithinAt_nonpos hderiv.hasFDerivWithinAt hone
  have hscalar :
      ((-scale * curve.dissipation s) -
        (-rate * curve.energy s)) ≤ 0 := by
    simpa using hnonpos
  linarith

/-- Forward direction of Chewi, Theorem 1.2.21, between arbitrary times. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem chewi_theorem_1_2_26_scalar_equivalence
    {C : ℝ} (hC : 0 < C) (curve : DissipationCurve 1) :
    (∀ s : ℝ,
      curve.energy s ≤ (C / 2) * curve.dissipation s) ↔
    (∀ s t : ℝ, 0 ≤ t →
      curve.energy (s + t) ≤
        curve.energy s * Real.exp (-(2 / C) * t)) := by
  constructor
  · intro hLSI s t ht
    have h := chewi_theorem_1_2_26_forward_from
      hC curve hLSI (show s ≤ s + t by linarith)
    simpa using h
  · exact chewi_theorem_1_2_26_backward hC curve

end

end SemigroupDecay
end FunctionalInequalities
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context