Samplinglib mathematical lesson

Actual global weighted resolvent scalar coercivity

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GlobalWeightedResolventCoercivity.global_weak_resolvent_coercivity · theorem · Teaching coverage

Read this first

Mathematical statement

Given the genuine source-neutral hypotheses, produce ONE actual u in the SAME original D.closure.domain for every positive epsilon and forcing, all-domain variational identity, local-volume L1 of u/G, ALL C1 compact ordinary weak-gradient products/identity, local squared PDE residual and compact-volume L2, ALL C2 compact ordinary weak-Poisson products/identity, and ALL C2 compact chi actual v/Gchi/Fchi volumeL2/support/weak identities. Derive m*norm(D.closureu)^2≤norm(f-epsilon*u)^2≤normf^2 by actual weighted radial cutoff/commutator convergence and true compact scalar inequalities, retaining zero dimension.

\[\exists u\in\operatorname{dom}\overline D:\quad\varepsilon\langle u,v\rangle+\langle\overline Du,\overline Dv\rangle=\langle f,v\rangle\ (\forall v),\quad m\|\overline Du\|_\mu^2\le\|f-\varepsilon u\|_\mu^2\le\|f\|_\mu^2.\]

Lean statement · global_weak_resolvent_coercivity

Given the genuine source-neutral hypotheses, produce ONE actual u in the SAME original D.closure.domain for every positive epsilon and forcing, all-domain variational identity, local-volume L1 of u/G, ALL C1 compact ordinary weak-gradient products/identity, local squared PDE residual and compact-volume L2, ALL C2 compact ordinary weak-Poisson products/identity, and ALL C2 compact chi actual v/Gchi/Fchi volumeL2/support/weak identities. Derive m*norm(D.closureu)^2<=norm(f-epsilon*u)^2<=normf^2 by actual weighted radial cutoff/commutator convergence and true compact scalar inequalities, retaining zero dimension.

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.

Download module (.lean)

theorem global_weak_resolvent_coercivity (W : E → ℝ) (hW : ContDiff ℝ 2 W)
    (hI : Integrable (fun x => Real.exp (-W x)))
    (hZ : 0 < ∫ x, Real.exp (-W x))
    (m M : ℝ) (hm : 0 < m) (hmM : m ≤ M)
    (hlower : ∀ x a, m*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ W) x a a)
    (hupper : ∀ x a, fderiv ℝ (fderiv ℝ W) x a a ≤ M*‖a‖^2)
    (μ : Measure E) (hμ : μ = (volume : Measure E).tilted (fun x => -W x)) :
    ∀ (D : Lp ℝ 2 μ →ₗ.[ℝ] Lp E 2 μ), D.IsClosable →
      (∀ (a : Lp ℝ 2 μ) (H : Lp E 2 μ), (a,H) ∈ D.graph ↔
        ∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
          a =ᵐ[μ] φ ∧ H =ᵐ[μ] gradient φ) →
      ∀ (ε : ℝ), 0 < ε → ∀ f : Lp ℝ 2 μ,
      ∃ u : D.closure.domain,
        (∀ v : D.closure.domain,
          ε * ⟪(u : Lp ℝ 2 μ), (v : Lp ℝ 2 μ)⟫ +
            ⟪D.closure u, D.closure v⟫ = ⟪f, (v : Lp ℝ 2 μ)⟫) ∧
        LocallyIntegrable (fun x => (u : Lp ℝ 2 μ) x) ∧
        LocallyIntegrable (fun x => D.closure u x) ∧
        (∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ → ∀ v : E,
          Integrable (fun x => ψ x * inner ℝ (D.closure u x) v) ∧
          Integrable (fun x => (u : Lp ℝ 2 μ) x * fderiv ℝ ψ x v) ∧
          (∫ x, ψ x * inner ℝ (D.closure u x) v) =
            - ∫ x, (u : Lp ℝ 2 μ) x * fderiv ℝ ψ x v) ∧
        LocallyIntegrable (fun x => ‖ε * (u : Lp ℝ 2 μ) x +
          inner ℝ (gradient W x) (D.closure u x) - f x‖ ^ 2) ∧
        (∀ K : Set E, IsCompact K →
          MemLp (fun x => (u : Lp ℝ 2 μ) x) 2 (volume.restrict K) ∧
          MemLp (fun x => D.closure u x) 2 (volume.restrict K) ∧
          MemLp (fun x => ε * (u : Lp ℝ 2 μ) x +
            inner ℝ (gradient W x) (D.closure u x) - f x) 2 (volume.restrict K)) ∧
        (∀ φ : E → ℝ, ContDiff ℝ 2 φ → HasCompactSupport φ →
          Integrable (fun x => (u : Lp ℝ 2 μ) x * Laplacian.laplacian φ x) ∧
          Integrable (fun x => (ε * (u : Lp ℝ 2 μ) x +
            inner ℝ (gradient W x) (D.closure u x) - f x) * φ x) ∧
          (∫ x, (u : Lp ℝ 2 μ) x * Laplacian.laplacian φ x) =
            ∫ x, (ε * (u : Lp ℝ 2 μ) x +
              inner ℝ (gradient W x) (D.closure u x) - f x) * φ x) ∧
        m*‖D.closure u‖^2 ≤ ‖f-ε • (u : Lp ℝ 2 μ)‖^2 ∧
        ‖f-ε • (u : Lp ℝ 2 μ)‖^2 ≤ ‖f‖^2 ∧
        ∀ χ : E → ℝ, ContDiff ℝ 2 χ → HasCompactSupport χ →
    let v := fun x => χ x * (u : Lp ℝ 2 μ) x
    let Gχ := fun x => χ x • D.closure u x + (u : Lp ℝ 2 μ) x • gradient χ x
    let Fχ := fun x => χ x * (ε * (u : Lp ℝ 2 μ) x + inner ℝ (gradient W x) (D.closure u x) - f x) + 2 * inner ℝ (gradient χ x) (D.closure u x) +
      (u : Lp ℝ 2 μ) x * Laplacian.laplacian χ x
    MemLp v 2 volume ∧ MemLp Gχ 2 volume ∧ MemLp Fχ 2 volume ∧
    tsupport v ⊆ tsupport χ ∧ tsupport Gχ ⊆ tsupport χ ∧ tsupport Fχ ⊆ tsupport χ ∧
    (∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ → ∀ a : E,
      Integrable (fun x => ψ x * inner ℝ (Gχ x) a) ∧
      Integrable (fun x => v x * fderiv ℝ ψ x a) ∧
      (∫ x, ψ x * inner ℝ (Gχ x) a) = -∫ x, v x * fderiv ℝ ψ x a) ∧
    ∀ φ : E → ℝ, ContDiff ℝ 2 φ → HasCompactSupport φ →
      Integrable (fun x => v x * Laplacian.laplacian φ x) ∧
      Integrable (fun x => Fχ x * φ x) ∧
      (∫ x, v x * Laplacian.laplacian φ x) = ∫ x, Fχ x * φ x

Exact module and namespace context

Proof roadmap

1Construct the original actual resolvent before choosing cutoffs
Consume LocalizedWeakResolvent on the SAME original closable exact compact-gradient graph. Its ONE u retains every local-volume/ordinary weak equation and every C2 cutoff equation. Set G=D.closureu and a=f-epsilon*u in genuine weighted L2. Do not assume the unlocalized inner(gradientW,G) or ordinary PDE residual is globally weighted L2.
2Derive linear drift and true scale-uniform cutoff bounds
The accepted Hessian secant integral and both source bounds imply norm(gradientW(x))≤b+M*normx, b=normgradientW0. Choose actual radial chi_n with radius n+1. Its true Riesz gradient bound C1/R, outer derivative zero and Laplacian trace bound C2/R^2 have constants before all radii. The second-derivative API is used only in the nontrivial branch; E0 is handled separately.
3Produce weighted L2 convergence through actual integrable squares
Bounded measurable coefficients times real/vector L2 functions are genuinely MemLp. Apply dominated integral convergence to squared norms and the true L2 norm-square integral; take square roots to get quotient convergence. Actual chi_n converges pointwise to1 and is in[0,1], hence chi_n*G and chi_n*a converge in weighted L2. Quotient subtraction is identified by explicit AE links.
4Control the drift commutator without an extra position moment
Outside normx≥2R the cutoff gradient vanishes. Inside, true linear drift gives a scale-uniform bound C1*(b+2M) for its drift product when R≥1. The generator coefficient c_n=inner(gradientW,gradientchi_n)-Deltachi_n is uniformly bounded and tends pointwise to0 by the actual derivative estimates. Dominated L2 then controls c_n*u using only weighted uL2, not norm(x)*u.
5Derive simultaneous actual localized gradient/generator limits
Use the genuine localized expressions Gchi=chiG+u*gradientchi and Fchi=chi*r+2inner(gradientchi,G)+u*Deltachi. Cancellation gives Achi=inner(gradientW,Gchi)-Fchi=chi*a-2inner(gradientchi,G)+c_n*u. The three errors are actual weighted MemLp/classes converging to0; thus Gchi→G and Achi→a. Preserve the sign and coefficient2; no separate global drift/PDE L2 premise is introduced.
6Apply actual compact coercivity and pass both squared norms
For each true smooth compact cutoff, pass its actual ordinary weak data to CompactWeightedPoissonCoercivity, which produces actual weighted AE classes, SAME original closure graph and scalar inequality. Identify these with the quotient classes of the true localized functions by AE extensionality. Pass norm and square limits to get the global scalar inequality. In E0, all vector L2 classes are zero, so the same inequality follows without the nontrivial derivative API.
7Test the SAME variational equation at u
The actual energy identity is epsilon*normu^2+normG^2=inner(f,u). Expand the residual squared norm using the real Hilbert identity; it equals normf^2-epsilon^2*normu^2-2epsilon*normG^2 and is at most normf^2. This positive-epsilon statement supplies no epsilon-zero limit, kernel theorem, Poincare, BL or main completion.

Full assumptions and notation

All objects and hypotheses

Finite real Hilbert/Borel E, including dimension0; canonical full-space volume. W is C2, exp(-W) genuinely integrable and Z positive. The actual input mu equals volume.tilted(-W). Real constants satisfy 0<m≤M and all-point/all-vector m*norma^2≤HessW(x)[a,a]≤M*norma^2. Both bounds are used to derive true linear drift.
Original weighted L2 partial real-linear gradient D is closable with its exact graph: actual AE classes of compact C-infinity functions and their genuine gradients. D precedes every epsilon>0 and f in L2(mu). No final closed-domain, generator-core, limit or coercivity certificate is given. The actual resolvent is constructed from this original graph.

Mathematical proof

1. Construct the original actual resolvent before choosing cutoffs

Consume LocalizedWeakResolvent on the SAME original closable exact compact-gradient graph. Its ONE u retains every local-volume/ordinary weak equation and every C2 cutoff equation. Set G=D.closureu and a=f-epsilon*u in genuine weighted L2. Do not assume the unlocalized inner(gradientW,G) or ordinary PDE residual is globally weighted L2.

\[a=f-\varepsilon u,\quad G=\overline Du,\quad r=\langle\nabla W,G\rangle-a.\]

Corresponding Lean step

LocalizedWeakResolvent.localized_weak_resolvent; global_weak_resolvent_coercivity

2. Derive linear drift and true scale-uniform cutoff bounds

The accepted Hessian secant integral and both source bounds imply norm(gradientW(x))≤b+M*normx, b=normgradientW0. Choose actual radial chi_n with radius n+1. Its true Riesz gradient bound C1/R, outer derivative zero and Laplacian trace bound C2/R^2 have constants before all radii. The second-derivative API is used only in the nontrivial branch; E0 is handled separately.

Corresponding Lean step

actual_linear_drift; actual_cutoff_gradient_estimates; actual_cutoff_laplacian_bound

3. Produce weighted L2 convergence through actual integrable squares

Bounded measurable coefficients times real/vector L2 functions are genuinely MemLp. Apply dominated integral convergence to squared norms and the true L2 norm-square integral; take square roots to get quotient convergence. Actual chi_n converges pointwise to1 and is in[0,1], hence chi_n*G and chi_n*a converge in weighted L2. Quotient subtraction is identified by explicit AE links.

\[\chi_nG\to G,\quad\chi_na\to a\quad\text{in }L^2(\mu).\]

Corresponding Lean step

bounded_coefficient_memLp; norm_sq_integral; bounded_coefficient_tendsto_zero; dominated_L2_tendsto_zero; actual_cutoff_function_convergence

4. Control the drift commutator without an extra position moment

Outside normx≥2R the cutoff gradient vanishes. Inside, true linear drift gives a scale-uniform bound C1*(b+2M) for its drift product when R≥1. The generator coefficient c_n=inner(gradientW,gradientchi_n)-Deltachi_n is uniformly bounded and tends pointwise to0 by the actual derivative estimates. Dominated L2 then controls c_n*u using only weighted uL2, not norm(x)*u.

\[|c_n(x)|\le C_1(b+2M)+C_2,\quad c_n(x)\to0,\quad c_nu\to0\text{ in }L^2(\mu).\]

Corresponding Lean step

actual_cutoff_generator_coefficient; actual_cutoff_commutators

5. Derive simultaneous actual localized gradient/generator limits

Use the genuine localized expressions Gchi=chiG+u*gradientchi and Fchi=chi*r+2inner(gradientchi,G)+u*Deltachi. Cancellation gives Achi=inner(gradientW,Gchi)-Fchi=chi*a-2inner(gradientchi,G)+c_n*u. The three errors are actual weighted MemLp/classes converging to0; thus Gchi→G and Achi→a. Preserve the sign and coefficient2; no separate global drift/PDE L2 premise is introduced.

\[A_{\chi_n}=\chi_na-2\langle\nabla\chi_n,G\rangle+c_nu\to a,\quad G_{\chi_n}\to G.\]

Corresponding Lean step

actual_cutoff_commutators; global_coercivity_from_localization

6. Apply actual compact coercivity and pass both squared norms

For each true smooth compact cutoff, pass its actual ordinary weak data to CompactWeightedPoissonCoercivity, which produces actual weighted AE classes, SAME original closure graph and scalar inequality. Identify these with the quotient classes of the true localized functions by AE extensionality. Pass norm and square limits to get the global scalar inequality. In E0, all vector L2 classes are zero, so the same inequality follows without the nontrivial derivative API.

\[m\|G_{\chi_n}\|_\mu^2\le\|A_{\chi_n}\|_\mu^2\ \Longrightarrow\ m\|G\|_\mu^2\le\|a\|_\mu^2.\]

Corresponding Lean step

CompactWeightedPoissonCoercivity.compact_weak_poisson_weighted_coercivity; global_coercivity_from_localization

7. Test the SAME variational equation at u

The actual energy identity is epsilon*normu^2+normG^2=inner(f,u). Expand the residual squared norm using the real Hilbert identity; it equals normf^2-epsilon^2*normu^2-2epsilon*normG^2 and is at most normf^2. This positive-epsilon statement supplies no epsilon-zero limit, kernel theorem, Poincare, BL or main completion.

\[\|f-\varepsilon u\|^2=\|f\|^2-\varepsilon^2\|u\|^2-2\varepsilon\|G\|^2\le\|f\|^2.\]

Corresponding Lean step

residual_norm_le; global_weak_resolvent_coercivity

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · global_weak_resolvent_coercivity

Construct the original actual resolvent before choosing cutoffs; Derive linear drift and true scale-uniform cutoff bounds; Produce weighted L2 convergence through actual integrable squares; Control the drift commutator without an extra position moment; Derive simultaneous actual localized gradient/generator limits; Apply actual compact coercivity and pass both squared norms; Test the SAME variational equation at u

Download module (.lean)

theorem global_weak_resolvent_coercivity (W : E → ℝ) (hW : ContDiff ℝ 2 W)
    (hI : Integrable (fun x => Real.exp (-W x)))
    (hZ : 0 < ∫ x, Real.exp (-W x))
    (m M : ℝ) (hm : 0 < m) (hmM : m ≤ M)
    (hlower : ∀ x a, m*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ W) x a a)
    (hupper : ∀ x a, fderiv ℝ (fderiv ℝ W) x a a ≤ M*‖a‖^2)
    (μ : Measure E) (hμ : μ = (volume : Measure E).tilted (fun x => -W x)) :
    ∀ (D : Lp ℝ 2 μ →ₗ.[ℝ] Lp E 2 μ), D.IsClosable →
      (∀ (a : Lp ℝ 2 μ) (H : Lp E 2 μ), (a,H) ∈ D.graph ↔
        ∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
          a =ᵐ[μ] φ ∧ H =ᵐ[μ] gradient φ) →
      ∀ (ε : ℝ), 0 < ε → ∀ f : Lp ℝ 2 μ,
      ∃ u : D.closure.domain,
        (∀ v : D.closure.domain,
          ε * ⟪(u : Lp ℝ 2 μ), (v : Lp ℝ 2 μ)⟫ +
            ⟪D.closure u, D.closure v⟫ = ⟪f, (v : Lp ℝ 2 μ)⟫) ∧
        LocallyIntegrable (fun x => (u : Lp ℝ 2 μ) x) ∧
        LocallyIntegrable (fun x => D.closure u x) ∧
        (∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ → ∀ v : E,
          Integrable (fun x => ψ x * inner ℝ (D.closure u x) v) ∧
          Integrable (fun x => (u : Lp ℝ 2 μ) x * fderiv ℝ ψ x v) ∧
          (∫ x, ψ x * inner ℝ (D.closure u x) v) =
            - ∫ x, (u : Lp ℝ 2 μ) x * fderiv ℝ ψ x v) ∧
        LocallyIntegrable (fun x => ‖ε * (u : Lp ℝ 2 μ) x +
          inner ℝ (gradient W x) (D.closure u x) - f x‖ ^ 2) ∧
        (∀ K : Set E, IsCompact K →
          MemLp (fun x => (u : Lp ℝ 2 μ) x) 2 (volume.restrict K) ∧
          MemLp (fun x => D.closure u x) 2 (volume.restrict K) ∧
          MemLp (fun x => ε * (u : Lp ℝ 2 μ) x +
            inner ℝ (gradient W x) (D.closure u x) - f x) 2 (volume.restrict K)) ∧
        (∀ φ : E → ℝ, ContDiff ℝ 2 φ → HasCompactSupport φ →
          Integrable (fun x => (u : Lp ℝ 2 μ) x * Laplacian.laplacian φ x) ∧
          Integrable (fun x => (ε * (u : Lp ℝ 2 μ) x +
            inner ℝ (gradient W x) (D.closure u x) - f x) * φ x) ∧
          (∫ x, (u : Lp ℝ 2 μ) x * Laplacian.laplacian φ x) =
            ∫ x, (ε * (u : Lp ℝ 2 μ) x +
              inner ℝ (gradient W x) (D.closure u x) - f x) * φ x) ∧
        m*‖D.closure u‖^2 ≤ ‖f-ε • (u : Lp ℝ 2 μ)‖^2 ∧
        ‖f-ε • (u : Lp ℝ 2 μ)‖^2 ≤ ‖f‖^2 ∧
        ∀ χ : E → ℝ, ContDiff ℝ 2 χ → HasCompactSupport χ →
    let v := fun x => χ x * (u : Lp ℝ 2 μ) x
    let Gχ := fun x => χ x • D.closure u x + (u : Lp ℝ 2 μ) x • gradient χ x
    let Fχ := fun x => χ x * (ε * (u : Lp ℝ 2 μ) x + inner ℝ (gradient W x) (D.closure u x) - f x) + 2 * inner ℝ (gradient χ x) (D.closure u x) +
      (u : Lp ℝ 2 μ) x * Laplacian.laplacian χ x
    MemLp v 2 volume ∧ MemLp Gχ 2 volume ∧ MemLp Fχ 2 volume ∧
    tsupport v ⊆ tsupport χ ∧ tsupport Gχ ⊆ tsupport χ ∧ tsupport Fχ ⊆ tsupport χ ∧
    (∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ → ∀ a : E,
      Integrable (fun x => ψ x * inner ℝ (Gχ x) a) ∧
      Integrable (fun x => v x * fderiv ℝ ψ x a) ∧
      (∫ x, ψ x * inner ℝ (Gχ x) a) = -∫ x, v x * fderiv ℝ ψ x a) ∧
    ∀ φ : E → ℝ, ContDiff ℝ 2 φ → HasCompactSupport φ →
      Integrable (fun x => v x * Laplacian.laplacian φ x) ∧
      Integrable (fun x => Fχ x * φ x) ∧
      (∫ x, v x * Laplacian.laplacian φ x) = ∫ x, Fχ x * φ x := by
  subst μ
  let μ := (volume : Measure E).tilted (fun x => -W x)
  dsimp only
  intro D hD hgraph ε hε f
  obtain ⟨u,hu,huL,hGL,hd,hr2,hl,hp,hcut⟩ :=
    AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.LocalizedWeakResolvent.localized_weak_resolvent
      W (hW.of_le (by norm_num)) hI D hD hgraph ε hε f
  let a := fun x => f x-ε*(u : Lp ℝ 2 μ) x
  have ha : MemLp a 2 μ := (Lp.memLp f).sub ((Lp.memLp (u : Lp ℝ 2 μ)).const_mul ε)
  have heq (x : E) : inner ℝ (gradient W x) (D.closure u x)-a x =
      ε*(u : Lp ℝ 2 μ) x+inner ℝ (gradient W x) (D.closure u x)-f x := by
    dsimp [a]; ring
  have hg := global_coercivity_from_localization W hW hI hZ m M hm hmM hlower hupper
    μ rfl D hD hgraph (fun x => (u : Lp ℝ 2 μ) x) a (fun x => D.closure u x)
    (Lp.memLp (u : Lp ℝ 2 μ)) ha (Lp.memLp (D.closure u)) (by
      intro χ hχ hc
      dsimp only
      simp_rw [heq]
      exact hcut χ hχ hc)
  have hgLp : (Lp.memLp (D.closure u)).toLp (fun x => D.closure u x) = D.closure u :=
    Lp.ext ((Lp.memLp (D.closure u)).coeFn_toLp)
  have haLp : ha.toLp a = f-ε • (u : Lp ℝ 2 μ) := by
    apply Lp.ext
    filter_upwards [ha.coeFn_toLp,Lp.coeFn_sub f (ε • (u : Lp ℝ 2 μ)),
      Lp.coeFn_smul ε (u : Lp ℝ 2 μ)] with x hx hy hz
    rw [hx,hy]
    change a x = f x-(ε • (u : Lp ℝ 2 μ)) x
    rw [hz]; rfl
  rw [hgLp,haLp] at hg
  have hen := hu u
  rw [real_inner_self_eq_norm_sq,real_inner_self_eq_norm_sq] at hen
  exact ⟨u,hu,huL,hGL,hd,hr2,hl,hp,hg,residual_norm_le f u (D.closure u) ε hε hen,hcut⟩

end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GlobalWeightedResolventCoercivity

Exact module and namespace context

Scope and omitted-condition boundaries

Same original compact-smooth gradient D precedes epsilon/f; derive ONE actual variational/localized resolvent u and actual weighted radial cutoff/commutator limits. Prove m*norm(D.closure u)^2≤norm(f-epsilon*u)^2≤normf^2 with source C2/two-sided0<m≤M Hessian bounds. E0 retained. No final limit/coercivity/core certificate, extra norm(x)*u moment, global ordinary Laplacian or drift-product L2, C-infinity potential, epsilon0/kernel/constant-domain/range/Poincare/BL/adjoint/core/jointselector/main/composition is inferred. Reflected quarter/fourfold constants exact; TV never transfers unbounded cost.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

tendsto_integral_of_dominated_convergence
memLp_two_iff_integrable_sq_norm
L2.inner_def
Lp.coeFn_sub
Lp.coeFn_smul
le_of_tendsto_of_tendsto
norm_sub_sq_real
MemLp.of_le_mul
Lp.ext
norm_inner_le_norm
real_inner_self_eq_norm_sq
real_inner_smul_right
LinearIsometryEquiv.norm_map
squeeze_zero
ContDiff.continuous_fderiv
ContDiff.of_le

Mathematical sources

PBPS AppendixC.1 authored analytic prerequisite — Same original compact-smooth gradient D precedes epsilon/f; derive ONE actual variational/localized resolvent u and actual weighted radial cutoff/commutator limits. Prove m*norm(D.closure u)^2<=norm(f-epsilon*u)^2<=normf^2 with source C2/two-sided0<m<=M Hessian bounds. E0 retained. No final limit/coercivity/core certificate, extra norm(x)*u moment, global ordinary Laplacian or drift-product L2, C-infinity potential, epsilon0/kernel/constant-domain/range/Poincare/BL/adjoint/core/jointselector/main/composition is inferred. Reflected quarter/fourfold constants exact; TV never transfers unbounded cost.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.