Source indexedlemma · leanprover/lean4:v4.33.0-rc1

ent_of_sum_le_ent_of_sum

PFR.MoreRuzsaDist · PFR/MoreRuzsaDist.lean:633 to 681

Source documentation

Let X₁, ..., Xₘ and Y₁, ..., Yₗ be tuples of jointly independent random variables (so the X's and Y's are also independent of each other), and let f : {1,..., l} → {1,... ,m} be a function, then H[∑ j, Y j] ≤ H[∑ i, X i] + ∑ j, H[Y j - X f(j)] - H[X_{f(j)}].

Exact Lean statement

lemma ent_of_sum_le_ent_of_sum {I : Type*} {s t : Finset I} (hdisj : Disjoint s t)
    (X : I → Ω → G) (hX : ∀ i, Measurable (X i)) [∀ i, FiniteRange (X i)]
    (hindep : iIndepFun X μ) (f : I → I) (hf : Finset.image f t ⊆ s) :
    H[∑ i ∈ t, X i; μ] ≤ H[∑ i ∈ s, X i; μ] + ∑ i ∈ t, (H[ X i - X (f i); μ] - H[X (f i); μ])

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ent_of_sum_le_ent_of_sum {I : Type*} {s t : Finset I} (hdisj : Disjoint s t)    (X : I → Ω → G) (hX : ∀ i, Measurable (X i)) [∀ i, FiniteRange (X i)]    (hindep : iIndepFun X μ) (f : I → I) (hf : Finset.image f t ⊆ s) :    H[∑ i ∈ t, X i; μ] ≤ H[∑ i ∈ s, X i; μ] + ∑ i ∈ t, (H[ X i - X (f i); μ] - H[X (f i); μ]) := by  --Write `W := $W := ∑_{i=1}^m X_i$`  set W := ∑ i ∈ s, X i with hW  --Write `U := ∑_{j=1}^l Y_j` (in the notation of the informal proof)  set U := ∑ i ∈ t, X i with hU  haveI : FiniteRange U := .finsum X  haveI : FiniteRange W := .finsum X  have U_meas : Measurable U := by    convert Finset.measurable_sum t (fun i _ => hX i)    simp only [hU, Finset.sum_apply]  have W_meas : Measurable W := by    convert Finset.measurable_sum s (fun i _ => hX i)    simp only [hW, Finset.sum_apply]  calc    --We have `H[U] ≤ H[-W + U]`    _ ≤ H[-W + U ; μ ] := entropy_sum_le_entropy_neg_add hdisj X hX hindep W_meas U_meas      -- `≤ H[-W] + ∑_{j=1}^l (H[-W + Y_j] - H[-W])`    _ ≤ H[-W ; μ] + ∑ i ∈ t, (H[-W + X i ; μ] - H[-W ; μ]) := by      apply entropy_kvm_decomposition hdisj      -- We'd want to give those to `apply` but this leads to timeouts...      · apply hX      · apply hindep    _ ≤ H[-W ; μ] + ∑ i ∈ t, (H[X i - X (f i) ; μ] - H[X (f i) ; μ]) := by      rw [add_le_add_iff_left]      apply Finset.sum_le_sum      intro i hi      calc        H[-W + X i ; μ] - H[-W ; μ]          = H[(- ∑ i ∈ s \ {f i}, X i) + (- (X (f i))) + X i; μ] - H[(- ∑ i ∈ s \ {f i}, X i) +            (- (X (f i))) ; μ]:= by          congr 3          all_goals            rw [hW, Finset.sum_sdiff_eq_sub, Finset.sum_singleton, neg_sub]            · abel            · rw [Finset.singleton_subset_iff]              apply hf (Finset.mem_image_of_mem _ hi)        _ ≤ H[(- (X <| f i)) + X i ; μ] - H[- (X (f i)) ; μ] :=          entropy_kvm_step hdisj hX hindep f hf i hi        _ = H[(- (X <| f i)) + X i ; μ] - H[(X (f i)) ; μ] := by          rw [entropy_neg (hX <| f i)]      apply le_of_eq      congr      abel    _ = H[W ; μ] + ∑ i ∈ t, (H[X i - X (f i); μ] - H[X (f i); μ]) := by      rw [entropy_neg]      measurability