Bounded binary probability-product entropy, including zero fibers

Mathematical statement

For arbitrary measurable spaces X,Y and actual probability laws mu,nu, let F be jointly measurable, nonnegative at every point, and bounded above by some real constant. Define Phi(t)=t log t, A(x)=integral F(x,y) dnu, B(y)=integral F(x,y) dmu, and m=integral F d(mu product nu). The actual joint function and its Phi transform are integrable, every fixed-coordinate slice and its Phi transform are integrable, and both actual marginals and their Phi transforms are integrable. The sum of the two marginal Phi integrals is at most the joint Phi integral plus Phi(m). Zero mass and zero fibers are included.

theorem bounded_product_entropy_subadditivity
    {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
    (μ : Measure X) (ν : Measure Y) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    (F : X × Y → ℝ) (hF : Measurable F)
    (hF0 : ∀ z, 0 ≤ F z) (hFb : ∃ C : ℝ, ∀ z, F z ≤ C) :
    let Φ : ℝ → ℝ := fun t => t * Real.log t
    let A : X → ℝ := fun x => ∫ y, F (x, y) ∂ν
    let B : Y → ℝ := fun y => ∫ x, F (x, y) ∂μ
    let m : ℝ := ∫ z, F z ∂μ.prod ν
    Integrable F (μ.prod ν) ∧
    Integrable (fun z => Φ (F z)) (μ.prod ν) ∧
    (∀ x, Integrable (fun y => F (x, y)) ν ∧
      Integrable (fun y => Φ (F (x, y))) ν) ∧
    (∀ y, Integrable (fun x => F (x, y)) μ ∧
      Integrable (fun x => Φ (F (x, y))) μ) ∧
    Integrable A μ ∧ Integrable B ν ∧
    Integrable (fun x => Φ (A x)) μ ∧ Integrable (fun y => Φ (B y)) ν ∧
    (∫ x, Φ (A x) ∂μ) + (∫ y, Φ (B y) ∂ν) ≤
      (∫ z, Φ (F z) ∂μ.prod ν) + Φ m

Proof roadmap

1. 1Produce the actual integration domains

   Bounded nonnegative measurable F is integrable on the finite product law and on each fixed-coordinate probability slice. Continuity of tlogt bounds Phi uniformly on the compact interval [0,C], producing the same domains for Phi(F). Strong measurability of the actual slice integral gives measurable A,B; probability normalization places them and m in [0,C], producing actual marginal Phi domains.

2. 2Construct a genuine positive comparison function

   Temporarily suppose delta≤F≤C with delta>0. Actual probability integrals give delta≤A,B,m. The function R(x,y)=A(x)B(y)/m is strictly positive and genuinely integrable. Fubini gives integral A=integral B=m, and the actual product-multiplication theorem yields integral R=m. No comparison-function mass certificate is supplied.

3. 3Use scalar logsum with the actual logarithm domains

   For a,b,c,m>0, apply u-1≤u log u to u=a/(bc/m), then multiply by the positive comparison value. Expand log products and division using actual nonzero arguments. This yields the pointwise inequality below. Because A,B lie in [delta,C], their logarithms are uniformly bounded; the F-weighted logs are genuinely integrable.

4. 4Integrate and use true weighted-log Fubini

   Integrate the pointwise inequality with all domains in hand. Genuine Fubini replaces integral F log A by integral A log A and integral F log B by integral B log B. Integral(F-R)=0 and integral F log m=m log m give the strict-positive product comparison. This is the sum-of-marginals inequality; two separate marginal KL bounds would not supply it.

5. 5Regularize without changing the public assumptions

   Set epsilon_n=1/(n+1) and F_n=F+epsilon_n. These are positive, bounded measurable functions. Actual slice and product integrability plus probability normalization give exactly A_n=A+epsilon_n, B_n=B+epsilon_n and m_n=m+epsilon_n. Apply the compiled positive comparison internally to each n.

6. 6Take only continuous entropy terms to the zero limit

   On [0,C+1], continuous Phi has a common finite bound. Dominated convergence for the actual finite laws sends the three Phi integrals to J_A,J_B,J_F; scalar continuity sends Phi(m+epsilon_n) to Phi(m), including m=0. Closed real order passes the inequality to the limit. Cross-log terms are never sent through a zero-fiber limit. Return the original actual domains together with this inequality.