Scaled Comparison of Sequential Relaxations

This is a general comparison principle for sequential relaxations.

Let $X$ and $Y$ be topological spaces, let $P$ and $Q$ be pre-energies on $X$ and $Y$, let $T:X\to Y$ be continuous, and let $\kappa\in[0,\infty)$ be an NNReal. Assume that every test $f$ of $P$ admits a test $g$ of $Q$ such that

and

Then, for every $x\in X$ with finite $P$-sequential relaxation,

This reusable lemma transports finite energy comparisons through continuous maps.

Formalization Note Energies and relaxations take values in $[0,\infty]$ (ENNReal), while $\kappa$ is coerced from NNReal; the finiteness premise excludes a top-valued source relaxation.

Original Lean declaration header

Within namespace FunctionalInequalities.Energy.PreEnergy. Shown in its original module context. Proof omitted.

theorem sequentialRelaxation_comp_le_mul {Y : Type*} [TopologicalSpace Y]
    (Q : PreEnergy Y) (T : X → Y) (hT : Continuous T) (κ : NNReal)
    (h : ∀ f : P.Test, ∃ g : Q.Test,
      Q.toAmbient g = T (P.toAmbient f) ∧ (Q.energy g : ENNReal) ≤ κ * P.energy f) (x : X)
    (hx : P.sequentialRelaxation x ≠ ⊤) :
    Q.sequentialRelaxation (T x) ≤ κ * P.sequentialRelaxation x

Module navigation

Module: Energy/Relaxation/Basic.

Definition modules: Energy/Form/Functional.

Source excerpt, lines 113–118 · Frozen source 408915f.