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

kvm_ineq_III

PFR.MoreRuzsaDist · PFR/MoreRuzsaDist.lean:464 to 487

Source documentation

If n ≥ 1 and X, Y₁, ..., Yₙ$ are jointly independent G-valued random variables, then d[Y i₀, ∑ i, Y i] ≤ d[Y i₀, Y i₁] + 2⁻¹ * (H[∑ i, Y i] - H[Y i₁]).

Exact Lean statement

lemma kvm_ineq_III {I : Type*} {i₀ i₁ : I} {s : Finset I}
    (hs₀ : ¬ i₀ ∈ s) (hs₁ : ¬ i₁ ∈ s) (h01 : i₀ ≠ i₁)
    (Y : I → Ω → G) [∀ i, FiniteRange (Y i)]
    (hY : ∀ i, Measurable (Y i)) (h_indep : iIndepFun Y μ) :
    d[Y i₀; μ # Y i₁ + ∑ i ∈ s, Y i; μ]
      ≤ d[Y i₀; μ # Y i₁; μ] + (2 : ℝ)⁻¹ * (H[Y i₁ + ∑ i ∈ s, Y i; μ] - H[Y i₁; μ])

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma kvm_ineq_III {I : Type*} {i₀ i₁ : I} {s : Finset I}    (hs₀ : ¬ i₀ ∈ s) (hs₁ : ¬ i₁ ∈ s) (h01 : i₀ ≠ i₁)    (Y : I → Ω → G) [∀ i, FiniteRange (Y i)]    (hY : ∀ i, Measurable (Y i)) (h_indep : iIndepFun Y μ) :    d[Y i₀; μ # Y i₁ + ∑ i ∈ s, Y i; μ]      ≤ d[Y i₀; μ # Y i₁; μ] + (2 : ℝ)⁻¹ * (H[Y i₁ + ∑ i ∈ s, Y i; μ] - H[Y i₁; μ]) := by  let J := Fin 3  let S : J → Finset I := ![{i₀}, {i₁}, s]  have h_dis : Set.univ.PairwiseDisjoint S := by    intro j _ k _ hjk    change Disjoint (S j) (S k)    fin_cases j <;> fin_cases k <;> try exact (hjk rfl).elim    all_goals      simp_all [Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one,        Finset.disjoint_singleton_right, S, h01.symm]  let φ : (j : J) → ((_ : S j) → G) → G    | 0 => fun Ys ↦ Ys ⟨i₀, by simp [S]⟩    | 1 => fun Ys ↦ Ys ⟨i₁, by simp [S]⟩    | 2 => fun Ys ↦ ∑ i : s, Ys ⟨i.1, i.2⟩  have hφ : (j : J) → Measurable (φ j) := fun j ↦ .of_discrete  have h_indep' : iIndepFun ![Y i₀, Y i₁, ∑ i ∈ s, Y i] μ := by    convert iIndepFun.finsets_comp S h_dis h_indep hY φ hφ with j x    fin_cases j <;> simp [φ, (s.sum_attach _).symm]  exact kvm_ineq_III_aux (hY i₀) (hY i₁) (by fun_prop) h_indep'