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

first_estimate

PFR.FirstEstimate · PFR/FirstEstimate.lean:143 to 153

Source documentation

We have $I_1 \leq 2 \eta k$

Exact Lean statement

lemma first_estimate
    [IsProbabilityMeasure (ℙ : Measure Ω₀₁)] [IsProbabilityMeasure (ℙ : Measure Ω₀₂)] :
    I₁ ≤ 2 * p.η * k

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma first_estimate    [IsProbabilityMeasure (ℙ : Measure Ω₀₁)] [IsProbabilityMeasure (ℙ : Measure Ω₀₂)] :    I₁ ≤ 2 * p.η * k := by  have v1 := rdist_add_rdist_add_condMutual_eq X₁ X₂ X₁' X₂' ‹_› ‹_› ‹_› ‹_› ‹_› ‹_› ‹_›  have v2 := rdist_of_sums_ge p X₁ X₂ X₁' X₂' ‹_› ‹_› ‹_› ‹_› ‹_›  have v3 := condRuzsaDist_of_sums_ge p X₁ X₂ X₁' X₂' ‹_› ‹_› ‹_› (by fun_prop) (by aesop)  have v4 := mul_le_mul_of_nonneg_left (diff_rdist_le_1 p X₁ X₂ X₁' X₂' ‹_› ‹_› ‹_› ‹_›) p.hη.le  have v5 := mul_le_mul_of_nonneg_left (diff_rdist_le_2 p X₁ X₂ X₁' X₂' ‹_› ‹_› ‹_› ‹_›) p.hη.le  have v6 := mul_le_mul_of_nonneg_left (diff_rdist_le_3 p X₁ X₂ X₁' X₂' ‹_› ‹_› ‹_› ‹_›) p.hη.le  have v7 := mul_le_mul_of_nonneg_left (diff_rdist_le_4 p X₁ X₂ X₁' X₂' ‹_› ‹_› ‹_› ‹_›) p.hη.le  linarith [v1, v2, v3, v4, v5, v6, v7]