Local-Density Region Lies In The Measure Support
ProvedFunctionalInequalities.Energy.SmoothGradient.LocalDensity.subset_support_readableThis lemma places the open local-density region inside the support of the probability measure.
Let be a normed additive group with a measurable Borel structure. Let be a probability measure on , let be an additive Haar measure, and let be a SmoothGradient.LocalDensity for . If denotes its designated open density region, then
The declaration is subset_support_readable. No inner-product, completeness, finite-dimensionality, or second-countability assumptions are included in the theorem type. The result is a support-membership fact used by the smooth-gradient density framework.
Original Lean declaration header
Within namespace FunctionalInequalities.Energy.SmoothGradient.LocalDensity. Shown in its original module context. Proof omitted.
theorem subset_support : D.Ω ⊆ (ν : Measure V).support
Module navigation
Module: Energy/SmoothGradient/Core.
Next: Test.exists_domain_sequence_tendsto.
Source excerpt, lines 93–93 · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_Energy_SmoothGradient_Core
open MeasureTheory Filter Topology
universe u
variable {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
[MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
variable {ν : MeasureTheory.ProbabilityMeasure V} {m : MeasureTheory.Measure V} (D : FunctionalInequalities.Energy.SmoothGradient.LocalDensity ν m)
variable [m.IsAddHaarMeasure]
omit [InnerProductSpace ℝ V] [CompleteSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
theorem FunctionalInequalities.Energy.SmoothGradient.LocalDensity.subset_support_readable : D.Ω ⊆ (ν : Measure V).support := by sorry