Local density hypotheses for smooth-gradient cores

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_WeightedGradient_Core
import Definitions.Def_KLSModular_FunctionalInequalities_Energy_WeightedGradient_Closable
import Definitions.Def_KLSModular_FunctionalInequalities_Energy_SmoothGradient_Intrinsic_Basic
import Definitions.Def_KLSModular_FunctionalInequalities_Energy_Relaxation_LowerSemicontinuous
import Definitions.Def_KLSModular_FunctionalInequalities_Energy_Form_Core
import Definitions.Def_KLSModular_FunctionalInequalities_L2_MeanVariance

noncomputable section
open MeasureTheory Filter Topology
open scoped ENNReal NNReal ContDiff
namespace FunctionalInequalities
namespace Energy
namespace SmoothGradient
universe u
variable {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
/-- Density hypotheses of the Blueprint: an open set `Ω` carrying `ν` on which `ν` has the
`m`-density `ρ`, positive almost everywhere with locally essentially bounded reciprocal. -/
structure LocalDensity (ν : ProbabilityMeasure V) (m : Measure V) where
  /-- The open set carrying the law. -/
  Ω : Set V
  isOpen : IsOpen Ω
  /-- The density on `Ω`. -/
  ρ : V → ℝ
  measurable : Measurable ρ
  /-- The complement of `Ω` is `ν`-null. -/
  compl_null : (ν : Measure V) Ωᶜ = 0
  /-- On Borel subsets of `Ω`, `ν` integrates `ρ` against `m`. -/
  restrict_eq : (ν : Measure V).restrict Ω =
    (m.restrict Ω).withDensity fun x ↦ ENNReal.ofReal (ρ x)
  /-- The density is positive almost everywhere on `Ω`. -/
  pos : ∀ᵐ x ∂m, x ∈ Ω → 0 < ρ x
  /-- The reciprocal of the density is essentially bounded on compact subsets of `Ω`. -/
  inv_locallyBounded : ∀ K : Set V, IsCompact K → K ⊆ Ω → ∃ C : ℝ, ∀ᵐ x ∂m, x ∈ K → (ρ x)⁻¹ ≤ C
namespace LocalDensity
variable {ν : ProbabilityMeasure V} {m : Measure V} (D : LocalDensity ν m)
omit [InnerProductSpace ℝ V] [CompleteSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V] in
/-- The law of a measurable subset of `Ω` is the integral of the density. -/
theorem measure_eq {s : Set V} (hs : MeasurableSet s) (hsΩ : s ⊆ D.Ω) :
    (ν : Measure V) s = ∫⁻ x in s, ENNReal.ofReal (D.ρ x) ∂m := by
  have h1 : (ν : Measure V) s = ((ν : Measure V).restrict D.Ω) s := by
    rw [Measure.restrict_apply hs, Set.inter_eq_self_of_subset_left hsΩ]
  rw [h1, D.restrict_eq, withDensity_apply _ hs, Measure.restrict_restrict hs,
    Set.inter_eq_self_of_subset_left hsΩ]
omit [InnerProductSpace ℝ V] [CompleteSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V] in
include D in
/-- The law is absolutely continuous with respect to `m`. -/
theorem absolutelyContinuous : (ν : Measure V) ≪ m := by
  refine Measure.AbsolutelyContinuous.mk fun s hs hs0 ↦ ?_
  have hsplit := measure_inter_add_sdiff (μ := (ν : Measure V)) s D.isOpen.measurableSet
  have h1 : (ν : Measure V) (s ∩ D.Ω) = 0 := by
    rw [D.measure_eq (hs.inter D.isOpen.measurableSet) Set.inter_subset_right]
    exact setLIntegral_measure_zero _ _ (measure_mono_null Set.inter_subset_left hs0)
  have h2 : (ν : Measure V) (s \ D.Ω) = 0 :=
    measure_mono_null (fun x hx ↦ hx.2) D.compl_null
  rw [← hsplit, h1, h2, add_zero]
variable [m.IsAddHaarMeasure]
end LocalDensity
section Agreement
variable (ν : ProbabilityMeasure V) (m : Measure V) [m.IsAddHaarMeasure] (D : LocalDensity ν m)
open Energy.WeightedGradient Energy.Euclidean
/-- The unit-weight gradient operator on globally Lipschitz tests, under the density
hypotheses. -/
def lipschitzOperator : Lp ℝ 2 (ν : Measure V) →ₗ.[ℝ] Lp V 2 (ν : Measure V) :=
  operator ν (ContinuousLinearMap.id ℝ V) D.absolutelyContinuous
omit [FiniteDimensional ℝ V] in
/-- The gradient of a smooth test is square integrable. -/
theorem Test.memLp_gradient (f : Test ν) : MemLp (gradient f.toFun) 2 (ν : Measure V) :=
  (memLp_two_iff_integrable_sq_norm (LipschitzApproximation.aestronglyMeasurable_gradient _ _)).mpr
    f.gradient_sq_integrable
end Agreement
end SmoothGradient
end Energy
end FunctionalInequalities