Samplinglib mathematical lesson

Actual Bochner means are controlled by the all-coupling quadratic cost

Read this first

Mathematical statement

Let U be any measurable space and H a complete real normed vector space. Let K:U→H be strongly measurable with ‖K(u)‖≤B. Let c:U×U→ℝ be measurable with 0≤c(z)≤C, and suppose ‖K(u)−K(v)‖≤L c(u,v), where B,C,L≥0. For any two probability measures μ,ν on U, define Q as the infimum, over all actual couplings π with these two marginals, of ∫c² dπ, interpreted as an extended nonnegative integral; set W=Q^(1/2). Then K is genuinely Bochner integrable under each law, Q is finite, and ‖∫K dμ−∫K dν‖≤L W.toReal. For every y∈H both residual norms are at most B+‖y‖. No optimizer, chosen-plan bound, finite-cost assumption or mean-identity premise is supplied. U need not carry a vector-space structure, and c need not be a metric.

\[Q=\inf_{\pi\in\Pi(\mu,\nu)}\int c(u,v)^2\,d\pi,\qquad \left\|\int K\,d\mu-\int K\,d\nu\right\|\le LQ^{1/2}<\infty.\]

Lean statement · bounded_bochner_mean_quadratic_transport_control

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 bounded_bochner_mean_quadratic_transport_control
    {U H : Type*} [MeasurableSpace U]
    [NormedAddCommGroup H] [NormedSpace ℝ H] [CompleteSpace H]
    (K : U → H) (hK : StronglyMeasurable K)
    (B C L : ℝ) (hB : 0 ≤ B) (hC : 0 ≤ C) (hL : 0 ≤ L)
    (hBound : ∀ u, ‖K u‖ ≤ B)
    (c : U × U → ℝ) (hc : Measurable c)
    (hc0 : ∀ z, 0 ≤ c z) (hcBound : ∀ z, c z ≤ C)
    (hLip : ∀ u v, ‖K u-K v‖ ≤ L * c (u,v))
    (μ ν : Measure U) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] :
    let cost : U × U → ℝ≥0∞ := fun z => ENNReal.ofReal ((c z)^2)
    let Q := AutoSamplingTheory.TechnicalLemmas.Measure.Transport.transportCost cost μ ν
    let W := Q ^ (1 / 2 : ℝ)
    Integrable K μ ∧ Integrable K ν ∧ Q ≠ ∞ ∧
      ‖(∫ u, K u ∂μ) - (∫ v, K v ∂ν)‖ ≤ L * W.toReal ∧
      ∀ y : H, ‖(∫ u, K u ∂μ)-y‖ ≤ B+‖y‖ ∧
        ‖(∫ v, K v ∂ν)-y‖ ≤ B+‖y‖

Exact module and namespace context

Read the complete claim and its hypotheses first, then open the numbered mathematical proof steps. Each step has an optional fold containing literal Lean implementation excerpts; the full theorem and module context remain available below.

Full assumptions and notation

All objects and hypotheses

U is measurable; H is a complete real normed vector space. μ and ν are actual probability measures.
K is strongly measurable and bounded by the nonnegative B. c is jointly measurable, nonnegative and bounded by nonnegative C.
L≥0 and the displayed feature increment bound holds for every pair; symmetry, a triangle inequality and an optimal coupling are not assumptions.

Mathematical proof

Open a step to read its argument and formula.

1. Produce integrability and finite transport cost

Strong measurability and the global norm bound give both Bochner integrals. The actual product probability μ⊗ν is a feasible coupling and has cost at most C², so Q is finite before toReal is used.

\[\int\|K\|\,d\mu,\int\|K\|\,d\nu\le B,\qquad Q\le\int c^2\,d(\mu\otimes\nu)\le C^2.\]

Corresponding Lean step

private theorem bounded_feature_integrable
    {U H : Type*} [MeasurableSpace U]
    [NormedAddCommGroup H] [NormedSpace ℝ H] [CompleteSpace H]
    (K : U → H) (hK : StronglyMeasurable K) (B : ℝ)
    (hBound : ∀ u, ‖K u‖ ≤ B) (μ : Measure U) [IsProbabilityMeasure μ] :
    Integrable K μ := by
  exact (integrable_const B).mono' hK.aestronglyMeasurable (ae_of_all _ hBound)

private theorem bounded_cost_lintegral
    {U : Type*} [MeasurableSpace U]
    (c : U × U → ℝ) (C : ℝ) (hC : 0 ≤ C)
    (hc0 : ∀ z, 0 ≤ c z) (hcBound : ∀ z, c z ≤ C)
    (γ : Measure (U × U)) [IsProbabilityMeasure γ] :
    (∫⁻ z, ENNReal.ofReal ((c z)^2) ∂γ) ≤ ENNReal.ofReal (C^2) := by
  calc
    (∫⁻ z, ENNReal.ofReal ((c z)^2) ∂γ) ≤ ∫⁻ _ : U × U, ENNReal.ofReal (C^2) ∂γ := by
      apply lintegral_mono
      intro z
      exact ENNReal.ofReal_le_ofReal ((sq_le_sq₀ (hc0 z) hC).2 (hcBound z))
    _ = ENNReal.ofReal (C^2) := by simp

private theorem actual_transport_cost_finite
    {U : Type*} [MeasurableSpace U]
    (c : U × U → ℝ) (C : ℝ) (hC : 0 ≤ C)
    (hc0 : ∀ z, 0 ≤ c z) (hcBound : ∀ z, c z ≤ C)
    (μ ν : Measure U) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] :
    AutoSamplingTheory.TechnicalLemmas.Measure.Transport.transportCost
      (fun z => ENNReal.ofReal ((c z)^2)) μ ν ≠ ∞ := by
  have h := AutoSamplingTheory.TechnicalLemmas.Measure.Transport.transportCost_le_lintegral_of_isCoupling
    (fun z => ENNReal.ofReal ((c z)^2)) μ ν (μ.prod ν)
    (AutoSamplingTheory.TechnicalLemmas.Measure.Transport.isCoupling_prod μ ν)
  exact ne_of_lt (lt_of_le_of_lt (h.trans (bounded_cost_lintegral c C hC hc0 hcBound _))
    ENNReal.ofReal_lt_top)

Literal implementation excerpt from AutoSamplingTheory/TechnicalLemmas/Measure/BochnerMeanTransport.lean. Local names retain their surrounding theorem context; the complete theorem and exact module context are folded below. These excerpts are presentation, not extra theorem premises.

2. Use the actual marginals for every coupling

Every feasible coupling is a probability. Marginal pushforward identities and Bochner subtraction express the actual mean difference as one integral of feature increments.

\[\int K\,d\mu-\int K\,d\nu=\int(K(u)-K(v))\,d\pi(u,v).\]

Corresponding Lean step

private theorem actual_coupling_mean_difference
    {U H : Type*} [MeasurableSpace U]
    [NormedAddCommGroup H] [NormedSpace ℝ H] [CompleteSpace H]
    (K : U → H) (hK : StronglyMeasurable K) (B : ℝ)
    (hBound : ∀ u, ‖K u‖ ≤ B)
    (μ ν : Measure U) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    (γ : Measure (U × U))
    (hγ : AutoSamplingTheory.TechnicalLemmas.Measure.Transport.IsCoupling γ μ ν) :
    (∫ u, K u ∂μ) - (∫ v, K v ∂ν) = ∫ z, (K z.1-K z.2) ∂γ := by
  letI : IsProbabilityMeasure γ :=
    AutoSamplingTheory.TechnicalLemmas.Measure.Transport.isProbabilityMeasure_of_isCoupling_left hγ
  have hleft : Integrable (fun z : U × U => K z.1) γ :=
    bounded_feature_integrable _ (hK.comp_measurable measurable_fst) B
      (fun z => hBound z.1) γ
  have hright : Integrable (fun z : U × U => K z.2) γ :=
    bounded_feature_integrable _ (hK.comp_measurable measurable_snd) B
      (fun z => hBound z.2) γ
  have hfst : (∫ u, K u ∂μ) = ∫ z, K z.1 ∂γ := by
    rw [← hγ.1]
    exact integral_map_of_stronglyMeasurable measurable_fst hK
  have hsnd : (∫ v, K v ∂ν) = ∫ z, K z.2 ∂γ := by
    rw [← hγ.2]
    exact integral_map_of_stronglyMeasurable measurable_snd hK
  rw [integral_sub hleft hright,← hfst,← hsnd]

3. Square the integral bound

The feature increment hypothesis first bounds the mean norm by L∫c dπ. Nonnegativity of ∫(c−∫c)² gives the probability square-integral inequality, without an assumed cost estimate.

\[\left(\int c\,d\pi\right)^2\le\int c^2\,d\pi,\qquad A^2\le L^2\int c^2\,d\pi,\quad A=\left\|\int K\,d\mu-\int K\,d\nu\right\|.\]

Corresponding Lean step

private theorem probability_square_integral_le
    {α : Type*} [MeasurableSpace α] (γ : Measure α) [IsProbabilityMeasure γ]
    (f : α → ℝ) (hf : MemLp f 2 γ) :
    (∫ x, f x ∂γ)^2 ≤ ∫ x, (f x)^2 ∂γ := by
  let m := ∫ x, f x ∂γ
  have hi : Integrable f γ := hf.integrable (by norm_num)
  have hs : Integrable (fun x => (f x)^2) γ := (memLp_two_iff_integrable_sq hf.1).1 hf
  have hm : Integrable (fun x => 2 * f x * m) γ := (hi.const_mul 2).mul_const m
  have hn : 0 ≤ ∫ x, (f x-m)^2 ∂γ := integral_nonneg fun x => sq_nonneg _
  have he : (∫ x, (f x-m)^2 ∂γ) = (∫ x, (f x)^2 ∂γ)-m^2 := by
    simp_rw [sub_sq]
    have hsub : Integrable (fun x => (f x)^2-2*f x*m) γ := hs.sub hm
    rw [integral_add hsub (integrable_const (m^2)),integral_sub hs hm]
    simp only [integral_mul_const,integral_const_mul,integral_const,probReal_univ,one_smul]
    change (∫ x, (f x)^2 ∂γ) - 2*m*m + m^2 = _
    ring
  rw [he] at hn
  change m^2 ≤ _
  linarith

private theorem actual_coupling_squared_mean_bound
    {U H : Type*} [MeasurableSpace U]
    [NormedAddCommGroup H] [NormedSpace ℝ H] [CompleteSpace H]
    (K : U → H) (hK : StronglyMeasurable K) (B C L : ℝ)
    (hC : 0 ≤ C) (hL : 0 ≤ L) (hBound : ∀ u, ‖K u‖ ≤ B)
    (c : U × U → ℝ) (hc : Measurable c)
    (hc0 : ∀ z, 0 ≤ c z) (hcBound : ∀ z, c z ≤ C)
    (hLip : ∀ u v, ‖K u-K v‖ ≤ L*c (u,v))
    (μ ν : Measure U) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    (γ : Measure (U × U))
    (hγ : AutoSamplingTheory.TechnicalLemmas.Measure.Transport.IsCoupling γ μ ν) :
    ‖(∫ u, K u ∂μ)-(∫ v, K v ∂ν)‖^2 ≤ L^2 * ∫ z, (c z)^2 ∂γ := by
  letI : IsProbabilityMeasure γ :=
    AutoSamplingTheory.TechnicalLemmas.Measure.Transport.isProbabilityMeasure_of_isCoupling_left hγ
  have hcLp : MemLp c 2 γ := (memLp_const C).mono' hc.aestronglyMeasurable
    (ae_of_all _ fun z => by simpa only [Real.norm_of_nonneg (hc0 z)] using hcBound z)
  have hcInt : Integrable c γ := hcLp.integrable (by norm_num)
  have hleft : Integrable (fun z : U × U => K z.1) γ := bounded_feature_integrable _
    (hK.comp_measurable measurable_fst) B (fun z => hBound z.1) γ
  have hright : Integrable (fun z : U × U => K z.2) γ := bounded_feature_integrable _
    (hK.comp_measurable measurable_snd) B (fun z => hBound z.2) γ
  have hnorm : ‖(∫ u, K u ∂μ)-(∫ v, K v ∂ν)‖ ≤ L * ∫ z, c z ∂γ := by
    rw [actual_coupling_mean_difference K hK B hBound μ ν γ hγ]
    calc
      ‖∫ z, (K z.1-K z.2) ∂γ‖ ≤ ∫ z, ‖K z.1-K z.2‖ ∂γ := norm_integral_le_integral_norm _
      _ ≤ ∫ z, L*c z ∂γ := integral_mono (hleft.sub hright).norm
        (hcInt.const_mul L) (fun z => hLip z.1 z.2)
      _ = L * ∫ z, c z ∂γ := integral_const_mul _ _
  have hm0 : 0 ≤ ∫ z, c z ∂γ := integral_nonneg hc0
  have hs := (sq_le_sq₀ (norm_nonneg _) (mul_nonneg hL hm0)).2 hnorm
  calc
    ‖(∫ u, K u ∂μ)-(∫ v, K v ∂ν)‖^2 ≤ (L * ∫ z, c z ∂γ)^2 := hs
    _ = L^2 * (∫ z, c z ∂γ)^2 := mul_pow _ _ _
    _ ≤ L^2 * ∫ z, (c z)^2 ∂γ := mul_le_mul_of_nonneg_left
      (probability_square_integral_le γ c hcLp) (sq_nonneg _)

4. Take the infimum over all feasible costs

For L>0, the same lower bound (A/L)² lies below every actual coupling cost. The order characterization of the extended-real infimum therefore places it below Q; no attainment or optimizer is used.

\[(A/L)^2\le\inf_{\pi\in\Pi(\mu,\nu)}\int c^2\,d\pi=Q.\]

Corresponding Lean step

    · have hLp : 0 < L := lt_of_le_of_ne hL (Ne.symm hL0)
      have hLow : ENNReal.ofReal ((A/L)^2) ≤ Q := by
        apply le_sInf
        rintro q ⟨γ,hγ,rfl⟩
        letI : IsProbabilityMeasure γ :=
          AutoSamplingTheory.TechnicalLemmas.Measure.Transport.isProbabilityMeasure_of_isCoupling_left hγ
        have hcLp : MemLp c 2 γ := (memLp_const C).mono' hc.aestronglyMeasurable
          (ae_of_all _ fun z => by simpa only [Real.norm_of_nonneg (hc0 z)] using hcBound z)
        have hcSq : Integrable (fun z => (c z)^2) γ := (memLp_two_iff_integrable_sq hcLp.1).1 hcLp
        change ENNReal.ofReal ((A/L)^2) ≤ ∫⁻ z, ENNReal.ofReal ((c z)^2) ∂γ
        rw [← ofReal_integral_eq_lintegral_ofReal hcSq (ae_of_all _ fun z => sq_nonneg _)]
        apply ENNReal.ofReal_le_ofReal
        rw [div_pow]
        apply (div_le_iff₀ (sq_pos_of_pos hLp)).2
        simpa only [mul_comm] using hs γ hγ

5. Handle the square root and the zero constant

Finiteness justifies the real conversion and the square-root identity. If L=0, the product-coupling squared bound already gives A=0 and no division is performed.

\[((Q^{1/2}).\mathrm{toReal})^2=Q.\mathrm{toReal},\qquad A\le L(Q^{1/2}).\mathrm{toReal}.\]

Corresponding Lean step

    · have h := hs (μ.prod ν)
        (AutoSamplingTheory.TechnicalLemmas.Measure.Transport.isCoupling_prod μ ν)
      rw [hL0] at *
      simp only [zero_mul,zero_pow (by decide : 2 ≠ 0)] at *
      change A^2 ≤ 0 at h
      nlinarith [norm_nonneg ((∫ u, K u ∂μ)-(∫ v, K v ∂ν))]

      have hReal := ENNReal.toReal_mono hQ hLow
      rw [ENNReal.toReal_ofReal (sq_nonneg _)] at hReal
      have he : (Q ^ (1 / 2 : ℝ))^2 = Q := by
        rw [← ENNReal.rpow_two,← ENNReal.rpow_mul]
        norm_num
      have heReal : ((Q ^ (1 / 2 : ℝ)).toReal)^2 = Q.toReal := by
        rw [← ENNReal.toReal_pow,he]
      have hr : A/L ≤ (Q ^ (1 / 2 : ℝ)).toReal := by
        have ha : 0 ≤ A/L := div_nonneg (norm_nonneg _) hL
        have hb := ENNReal.toReal_nonneg (a := Q ^ (1 / 2 : ℝ))
        nlinarith
      calc
        A = L * (A/L) := by field_simp
        _ ≤ L * (Q ^ (1 / 2 : ℝ)).toReal := mul_le_mul_of_nonneg_left hr hL

6. Bound both residuals

The norm of each actual mean is at most B. The triangle inequality gives the two bounds for the same arbitrary fixed y.

\[\left\|\int K\,d\mu-y\right\|,\left\|\int K\,d\nu-y\right\|\le B+\|y\|.\]

Corresponding Lean step

  · have hmμ : ‖∫ u, K u ∂μ‖ ≤ B := by
      simpa only [probReal_univ,mul_one] using
        (norm_integral_le_of_norm_le_const (μ := μ) (ae_of_all _ hBound))
    have hmν : ‖∫ v, K v ∂ν‖ ≤ B := by
      simpa only [probReal_univ,mul_one] using
        (norm_integral_le_of_norm_le_const (μ := ν) (ae_of_all _ hBound))
    intro y
    exact ⟨(norm_sub_le _ _).trans (add_le_add hmμ le_rfl),
      (norm_sub_le _ _).trans (add_le_add hmν le_rfl)⟩

Lean verification

Lean proof · bounded_bochner_mean_quadratic_transport_control

The displayed formula proof explains the mathematical route; the exact Lean is folded adjacent.

Download module (.lean)

theorem bounded_bochner_mean_quadratic_transport_control
    {U H : Type*} [MeasurableSpace U]
    [NormedAddCommGroup H] [NormedSpace ℝ H] [CompleteSpace H]
    (K : U → H) (hK : StronglyMeasurable K)
    (B C L : ℝ) (hB : 0 ≤ B) (hC : 0 ≤ C) (hL : 0 ≤ L)
    (hBound : ∀ u, ‖K u‖ ≤ B)
    (c : U × U → ℝ) (hc : Measurable c)
    (hc0 : ∀ z, 0 ≤ c z) (hcBound : ∀ z, c z ≤ C)
    (hLip : ∀ u v, ‖K u-K v‖ ≤ L * c (u,v))
    (μ ν : Measure U) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] :
    let cost : U × U → ℝ≥0∞ := fun z => ENNReal.ofReal ((c z)^2)
    let Q := AutoSamplingTheory.TechnicalLemmas.Measure.Transport.transportCost cost μ ν
    let W := Q ^ (1 / 2 : ℝ)
    Integrable K μ ∧ Integrable K ν ∧ Q ≠ ∞ ∧
      ‖(∫ u, K u ∂μ) - (∫ v, K v ∂ν)‖ ≤ L * W.toReal ∧
      ∀ y : H, ‖(∫ u, K u ∂μ)-y‖ ≤ B+‖y‖ ∧
        ‖(∫ v, K v ∂ν)-y‖ ≤ B+‖y‖ := by
  dsimp only
  let cost : U × U → ℝ≥0∞ := fun z => ENNReal.ofReal ((c z)^2)
  let Q := AutoSamplingTheory.TechnicalLemmas.Measure.Transport.transportCost cost μ ν
  have hQ : Q ≠ ∞ := actual_transport_cost_finite c C hC hc0 hcBound μ ν
  have hμ : Integrable K μ := bounded_feature_integrable K hK B hBound μ
  have hν : Integrable K ν := bounded_feature_integrable K hK B hBound ν
  have hs (γ : Measure (U × U))
      (hγ : AutoSamplingTheory.TechnicalLemmas.Measure.Transport.IsCoupling γ μ ν) :
      ‖(∫ u, K u ∂μ)-(∫ v, K v ∂ν)‖^2 ≤ L^2 * ∫ z, (c z)^2 ∂γ :=
    actual_coupling_squared_mean_bound K hK B C L hC hL hBound c hc hc0 hcBound hLip μ ν γ hγ
  refine ⟨hμ,hν,hQ,?_,?_⟩
  · let A := ‖(∫ u, K u ∂μ)-(∫ v, K v ∂ν)‖
    change A ≤ L * (Q ^ (1 / 2 : ℝ)).toReal
    by_cases hL0 : L = 0
    · have h := hs (μ.prod ν)
        (AutoSamplingTheory.TechnicalLemmas.Measure.Transport.isCoupling_prod μ ν)
      rw [hL0] at *
      simp only [zero_mul,zero_pow (by decide : 2 ≠ 0)] at *
      change A^2 ≤ 0 at h
      nlinarith [norm_nonneg ((∫ u, K u ∂μ)-(∫ v, K v ∂ν))]
    · have hLp : 0 < L := lt_of_le_of_ne hL (Ne.symm hL0)
      have hLow : ENNReal.ofReal ((A/L)^2) ≤ Q := by
        apply le_sInf
        rintro q ⟨γ,hγ,rfl⟩
        letI : IsProbabilityMeasure γ :=
          AutoSamplingTheory.TechnicalLemmas.Measure.Transport.isProbabilityMeasure_of_isCoupling_left hγ
        have hcLp : MemLp c 2 γ := (memLp_const C).mono' hc.aestronglyMeasurable
          (ae_of_all _ fun z => by simpa only [Real.norm_of_nonneg (hc0 z)] using hcBound z)
        have hcSq : Integrable (fun z => (c z)^2) γ := (memLp_two_iff_integrable_sq hcLp.1).1 hcLp
        change ENNReal.ofReal ((A/L)^2) ≤ ∫⁻ z, ENNReal.ofReal ((c z)^2) ∂γ
        rw [← ofReal_integral_eq_lintegral_ofReal hcSq (ae_of_all _ fun z => sq_nonneg _)]
        apply ENNReal.ofReal_le_ofReal
        rw [div_pow]
        apply (div_le_iff₀ (sq_pos_of_pos hLp)).2
        simpa only [mul_comm] using hs γ hγ
      have hReal := ENNReal.toReal_mono hQ hLow
      rw [ENNReal.toReal_ofReal (sq_nonneg _)] at hReal
      have he : (Q ^ (1 / 2 : ℝ))^2 = Q := by
        rw [← ENNReal.rpow_two,← ENNReal.rpow_mul]
        norm_num
      have heReal : ((Q ^ (1 / 2 : ℝ)).toReal)^2 = Q.toReal := by
        rw [← ENNReal.toReal_pow,he]
      have hr : A/L ≤ (Q ^ (1 / 2 : ℝ)).toReal := by
        have ha : 0 ≤ A/L := div_nonneg (norm_nonneg _) hL
        have hb := ENNReal.toReal_nonneg (a := Q ^ (1 / 2 : ℝ))
        nlinarith
      calc
        A = L * (A/L) := by field_simp
        _ ≤ L * (Q ^ (1 / 2 : ℝ)).toReal := mul_le_mul_of_nonneg_left hr hL
  · have hmμ : ‖∫ u, K u ∂μ‖ ≤ B := by
      simpa only [probReal_univ,mul_one] using
        (norm_integral_le_of_norm_le_const (μ := μ) (ae_of_all _ hBound))
    have hmν : ‖∫ v, K v ∂ν‖ ≤ B := by
      simpa only [probReal_univ,mul_one] using
        (norm_integral_le_of_norm_le_const (μ := ν) (ae_of_all _ hBound))
    intro y
    exact ⟨(norm_sub_le _ _).trans (add_le_add hmμ le_rfl),
      (norm_sub_le _ _).trans (add_le_add hmν le_rfl)⟩

end AutoSamplingTheory.TechnicalLemmas.Measure.BochnerMeanTransport

Exact module and namespace context

Scope and omitted-condition boundaries

The all-coupling infimum is literal extended nonnegative transportCost; real conversion occurs after finite cost is proved. No optimal coupling or attainment is assumed.
This is a generic bounded-cost theorem. A round-geodesic metric identification, a concrete Gaussian feature Lipschitz estimate, and their particular Wasserstein instance must be established separately.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Pinned Mathlib Bochner integration, marginal maps and extended-real order

Mathematical sources

Samplinglib original feature differentiation and transport supplement v1 (2026-10-21) (historical source) — Original generic mathematical supplement from the cited pinned library prerequisites; no primary-textbook theorem or statistical convergence credit.

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