Leibniz Rule For The Closed Weighted Gradient

This theorem extends the product rule to every element of the closed weighted-gradient domain.

Let $V$ be finite-dimensional with the stated structures, let $m$ be an additive Haar measure, let $\nu$ be log-concave with nonempty interior support, and let $B:V\to V$ be continuous linear. For a smooth compactly supported multiplier $\phi:V\to\mathbb R$ and any

there exists a proof of domain membership for the $L^2(\nu)$ class of $\phi x$, and the resulting operator value satisfies, $\nu$-almost everywhere,

The statement uses toLp for the product class and closedWeightedOperator for the closed operator. No boundedness or differentiability of $x$ is assumed.

Original Lean declaration header

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

theorem exists_mem_domain_closedWeightedOperator_toLp_mul {φ : V → ℝ} (hφ : ContDiff ℝ ∞ φ)
    (hφc : HasCompactSupport φ) (x : (hν.closedWeightedOperator m B hi).domain) :
    ∃ hmem : (memLp_mul_of_contDiff_hasCompactSupport (ν := ν) hφ hφc
        (x : Lp ℝ 2 (ν : Measure V))).toLp _ ∈ (hν.closedWeightedOperator m B hi).domain,
      ((hν.closedWeightedOperator m B hi ⟨_, hmem⟩ : Lp V 2 (ν : Measure V)) : V → V)
        =ᵐ[(ν : Measure V)] fun y =>
          φ y • ((hν.closedWeightedOperator m B hi x : Lp V 2 (ν : Measure V)) : V → V) y
            + (x : Lp ℝ 2 (ν : Measure V)) y • apply B φ y

Module navigation

Module: KLS/LogConcave/WeightedGradient/Multiplier.

Definition modules: KLS/LogConcave/WeightedGradient/Closure, Probability/LogConcave, Energy/WeightedGradient/Basic.

Supporting theorems: exists_seq_smooth_tendsto_graph.

Previous: exists_seq_smooth_tendsto_graph.

Source excerpt, lines 134–141 · Frozen source 408915f.