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

single_fibres

PFR.WeakPFR · PFR/WeakPFR.lean:431 to 582

Source documentation

Let $\phi : G\to H$ be a homomorphism and $A,B\subseteq G$ be finite subsets. If $x,y\in H$ then let $A_x=A\cap \phi^{-1}(x)$ and $B_y=B\cap \phi^{-1}(y)$ . There exist $x,y\in H$ such that $A_x,B_y$ are both non-empty and [d[\phi(U_A);\phi(U_B)]\log \frac{\lvert A\rvert\lvert B\rvert}{\lvert A_x\rvert\lvert B_y\rvert} \leq (\mathbb{H}(\phi(U_A))+\mathbb{H}(\phi(U_B)))(d(U_A,U_B)-d(U_{A_x},U_{B_y}).]

Exact Lean statement

lemma single_fibres {G H Ω Ω' : Type*}
    [AddCommGroup G] [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G]
    [AddCommGroup H] [Countable H] [MeasurableSpace H] [MeasurableSingletonClass H]
    [MeasureSpace Ω] [MeasureSpace Ω']
    [IsProbabilityMeasure (ℙ : Measure Ω)] [IsProbabilityMeasure (ℙ : Measure Ω')] (φ : G →+ H)
    {A B : Set G} [Finite A] [Finite B] {UA : Ω → G} {UB : Ω' → G}
    (hA : A.Nonempty) (hB : B.Nonempty)
    (hUA' : Measurable UA) (hUB' : Measurable UB) (hUA : IsUniform A UA) (hUB : IsUniform B UB)
    (hUA_mem : ∀ ω, UA ω ∈ A) (hUB_mem : ∀ ω, UB ω ∈ B) :
    ∃ (x y : H) (Ax By : Set G),
      Ax = A ∩ φ.toFun ⁻¹' {x} ∧ By = B ∩ φ.toFun ⁻¹' {y} ∧ Ax.Nonempty ∧ By.Nonempty ∧
      d[φ.toFun ∘ UA # φ.toFun ∘ UB]
      * log (Nat.card A * Nat.card B / ((Nat.card Ax) * (Nat.card By))) ≤
      (H[φ.toFun ∘ UA] + H[φ.toFun ∘ UB]) * (d[UA # UB] - dᵤ[Ax # By])

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma single_fibres {G H Ω Ω' : Type*}    [AddCommGroup G] [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G]    [AddCommGroup H] [Countable H] [MeasurableSpace H] [MeasurableSingletonClass H]    [MeasureSpace Ω] [MeasureSpace Ω']    [IsProbabilityMeasure (ℙ : Measure Ω)] [IsProbabilityMeasure (ℙ : Measure Ω')] (φ : G →+ H)    {A B : Set G} [Finite A] [Finite B] {UA : Ω → G} {UB : Ω' → G}    (hA : A.Nonempty) (hB : B.Nonempty)    (hUA' : Measurable UA) (hUB' : Measurable UB) (hUA : IsUniform A UA) (hUB : IsUniform B UB)    (hUA_mem : ∀ ω, UA ω ∈ A) (hUB_mem : ∀ ω, UB ω ∈ B) :    ∃ (x y : H) (Ax By : Set G),      Ax = A ∩ φ.toFun ⁻¹' {x} ∧ By = B ∩ φ.toFun ⁻¹' {y} ∧ Ax.Nonempty ∧ By.Nonempty ∧      d[φ.toFun ∘ UA # φ.toFun ∘ UB]      * log (Nat.card A * Nat.card B / ((Nat.card Ax) * (Nat.card By))) ≤      (H[φ.toFun ∘ UA] + H[φ.toFun ∘ UB]) * (d[UA # UB] - dᵤ[Ax # By]) := by  have : Nonempty A := hA.to_subtype  have : Nonempty B := hB.to_subtype  have : FiniteRange UA := finiteRange_of_finset UA A.toFinite.toFinset (by simpa)  have : FiniteRange UB := finiteRange_of_finset UB B.toFinite.toFinset (by simpa)  have hUA_coe : IsUniform A.toFinite.toFinset UA := by rwa [Set.Finite.coe_toFinset]  have hUB_coe : IsUniform B.toFinite.toFinset UB := by rwa [Set.Finite.coe_toFinset]  let A_ (x : H) : Set G := A ∩ φ.toFun ⁻¹' {x}  let B_ (y : H) : Set G := B ∩ φ.toFun ⁻¹' {y}  let X : Finset H := FiniteRange.toFinset (φ.toFun ∘ UA)  let Y : Finset H := FiniteRange.toFinset (φ.toFun ∘ UB)  have h_Ax (x : X) : Nonempty (A_ x.val) := by    obtain ⟨ω, hω⟩ := (FiniteRange.mem_iff _ _).mp x.property    use UA ω; exact Set.mem_inter (hUA_mem ω) hω  have h_By (y : Y) : Nonempty (B_ y.val) := by    obtain ⟨ω, hω⟩ := (FiniteRange.mem_iff _ _).mp y.property    use UB ω; exact Set.mem_inter (hUB_mem ω) hω  have h_AX (a : A) : φ.toFun a.val ∈ X := by    obtain ⟨ω, hω⟩ := hUA_coe.nonempty_preimage_of_mem hUA' (A.toFinite.mem_toFinset.mpr a.property)    exact (FiniteRange.mem_iff _ (φ.toFun a.val)).mpr ⟨ω, congr_arg _ hω⟩  have h_BY (b : B) : φ.toFun b.val ∈ Y := by    obtain ⟨ω, hω⟩ := hUB_coe.nonempty_preimage_of_mem hUB' (B.toFinite.mem_toFinset.mpr b.property)    exact (FiniteRange.mem_iff _ (φ.toFun b.val)).mpr ⟨ω, congr_arg _ hω⟩  let φ_AX (a : A) : X := by use φ.toFun a.val; exact h_AX a  let φ_BY (b : B) : Y := by use φ.toFun b.val; exact h_BY b  have h_φ_AX (x : X) : A_ x.val = φ_AX ⁻¹' {x} := by ext; simp [A_, φ_AX]; simp [Subtype.ext_iff]  have h_φ_BY (y : Y) : B_ y.val = φ_BY ⁻¹' {y} := by ext; simp [B_, φ_BY]; simp [Subtype.ext_iff]  let p (x : H) (y : H) : ℝ :=    (Nat.card (A_ x).Elem) * (Nat.card (B_ y).Elem) / ((Nat.card A.Elem) * (Nat.card B.Elem))  have :    ∑ x ∈ X, ∑ y ∈ Y, (p x y) * dᵤ[A_ x # B_ y] ≤ d[UA # UB] - d[φ.toFun ∘ UA # φ.toFun ∘ UB] :=  calc    _ = d[UA | φ.toFun ∘ UA # UB | φ.toFun ∘ UB] := by      rewrite [condRuzsaDist_eq_sum hUA' (.comp .of_discrete hUA')        hUB' (.comp .of_discrete hUB')]      refine Finset.sum_congr rfl <| fun x hx ↦ Finset.sum_congr rfl <| fun y hy ↦ ?_      have : Nonempty (A_ x) := h_Ax ⟨x, hx⟩      have : Nonempty (B_ y) := h_By ⟨y, hy⟩      let μx := (ℙ : Measure Ω)[|(φ.toFun ∘ UA) ⁻¹' {x}]      have hμx : IsProbabilityMeasure μx := by        apply ProbabilityTheory.cond_isProbabilityMeasure        rw [Set.preimage_comp]        apply hUA_coe.measure_preimage_ne_zero hUA'        rw [Set.inter_comm, Set.Finite.coe_toFinset]        exact .of_subtype      let μy := (ℙ : Measure Ω')[|(φ.toFun ∘ UB) ⁻¹' {y}]      have hμy : IsProbabilityMeasure μy := by        apply ProbabilityTheory.cond_isProbabilityMeasure        rw [Set.preimage_comp]        apply hUB_coe.measure_preimage_ne_zero hUB'        rw [Set.inter_comm, Set.Finite.coe_toFinset]        exact .of_subtype      have h_μ_unif : IsUniform (A_ x) UA μx ∧ IsUniform (B_ y) UB μy := by        have : _ ∧ _ := ⟨hUA.restrict hUA' (φ.toFun ⁻¹' {x}), hUB.restrict hUB' (φ.toFun ⁻¹' {y})⟩        rwa [Set.inter_comm _ A, Set.inter_comm _ B] at this      rw [setRuzsaDist_eq_rdist h_μ_unif.1 h_μ_unif.2 hUA' hUB']      change _ = (Measure.real _ (UA ⁻¹' (_ ⁻¹' _))) * (Measure.real _ (UB ⁻¹' (_ ⁻¹' _))) * _      rewrite [hUA_coe.measureReal_preimage hUA', hUB_coe.measureReal_preimage hUB']      simp_rw [p, A_, B_, probReal_univ, one_mul]      rewrite [mul_div_mul_comm, Set.inter_comm A, Set.inter_comm B]      simp only [Set.Finite.coe_toFinset, Set.Finite.mem_toFinset]; rfl    _ ≤ d[UA # UB] - d[φ.toFun ∘ UA # φ.toFun ∘ UB] := by      rewrite [ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe]      linarith only [rdist_le_sum_fibre φ hUA' hUB' (μ := ℙ) (μ' := ℙ)]  let M := H[φ.toFun ∘ UA] + H[φ.toFun ∘ UB]  have hM : M = ∑ x ∈ X, ∑ y ∈ Y, Real.negMulLog (p x y) := by    have h_compl {x y} (h_notin : (x, y) ∉ X ×ˢ Y) : Real.negMulLog (p x y) = 0 := by      unfold p      rewrite [Finset.mem_product, not_and_or] at h_notin      suffices A_ x = ∅ ∨ B_ y = ∅ by obtain h | h := this <;> rw [h] <;> simp      refine h_notin.imp ?_ ?_      · rw [← not_nonempty_iff_eq_empty]        rintro h ⟨a, ha, rfl⟩        exact h (h_AX ⟨a, ha⟩)      · rw [← not_nonempty_iff_eq_empty]        rintro h ⟨a, ha, rfl⟩        exact h (h_BY ⟨a, ha⟩)    unfold M    unfold entropy    have : IsProbabilityMeasure (.map (φ ∘ UA) ℙ) :=      Measure.isProbabilityMeasure_map (.comp_measurable .of_discrete hUA')    have : IsProbabilityMeasure (.map (φ ∘ UB) ℙ) :=      Measure.isProbabilityMeasure_map (.comp_measurable .of_discrete hUB')    rewrite [← Finset.sum_product',      ← tsum_eq_sum (L := SummationFilter.unconditional _) fun _ ↦ h_compl, ← measureEntropy_prod]    apply tsum_congr; intro; congr    rewrite [← Set.singleton_prod_singleton, measureReal_ennreal_smul_apply, measureReal_def,      Measure.prod_prod,      Measure.map_apply (.comp .of_discrete hUA') (MeasurableSet.singleton _),      Measure.map_apply (.comp .of_discrete hUB') (MeasurableSet.singleton _),      Set.preimage_comp, hUA_coe.measure_preimage hUA',      Set.preimage_comp, hUB_coe.measure_preimage hUB']    simp [p, A_, B_, mul_div_mul_comm, Set.inter_comm, ENNReal.toReal_div]  have h_sum : ∑ x ∈ X, ∑ y ∈ Y,      (p x y) * (M * dᵤ[A_ x # B_ y] + d[φ.toFun ∘ UA # φ.toFun ∘ UB] * -Real.log (p x y)) ≤      M * d[UA # UB] :=  calc    _ = ∑ x ∈ X, ∑ y ∈ Y, (p x y) * M * dᵤ[A_ x # B_ y] + M * d[φ.toFun ∘ UA # φ.toFun ∘ UB] := by      simp_rw [hM, Finset.sum_mul, ← Finset.sum_add_distrib]      refine Finset.sum_congr rfl <| fun _ _ ↦ Finset.sum_congr rfl <| fun _ _ ↦ ?_      simp only [negMulLog, left_distrib, mul_assoc, Finset.sum_mul]      exact congrArg (HAdd.hAdd _) (by group)    _ = M * ∑ x ∈ X, ∑ y ∈ Y, (p x y) * dᵤ[A_ x # B_ y] + M * d[φ.toFun ∘ UA # φ.toFun ∘ UB] := by      simp_rw [Finset.mul_sum]      congr; ext; congr; ext; group    _ ≤ M * d[UA # UB] := by      rewrite [← left_distrib]      apply mul_le_mul_of_nonneg_left      · linarith      · unfold M        linarith only [entropy_nonneg (φ.toFun ∘ UA) ℙ, entropy_nonneg (φ.toFun ∘ UB) ℙ]  have : ∃ x : X, ∃ y : Y,      M * dᵤ[A_ x.val # B_ y.val] + d[φ.toFun ∘ UA # φ.toFun ∘ UB] * -Real.log (p x.val y.val) ≤      M * d[UA # UB] := by    let f (xy : H × H) := (p xy.1 xy.2) * (M * d[UA # UB])    let g (xy : H × H) := (p xy.1 xy.2) *      (M * dᵤ[A_ xy.1 # B_ xy.2] + d[φ.toFun ∘ UA # φ.toFun ∘ UB] * -Real.log (p xy.1 xy.2))    by_contra hc; push Not at hc    replace hc : ∀ xy ∈ X ×ˢ Y, f xy < g xy := by      refine fun xy h ↦ mul_lt_mul_of_pos_left ?_ ?_      · exact hc ⟨xy.1, (Finset.mem_product.mp h).1⟩ ⟨xy.2, (Finset.mem_product.mp h).2⟩      · have : Nonempty _ := h_Ax ⟨xy.1, (Finset.mem_product.mp h).1⟩        have : Nonempty _ := h_By ⟨xy.2, (Finset.mem_product.mp h).2⟩        simp only [p, div_pos, mul_pos, Nat.cast_pos, Nat.card_pos]    have h_nonempty : Finset.Nonempty (X ×ˢ Y) := by      use ⟨φ.toFun <| UA <| Classical.choice <| ProbabilityMeasure.nonempty ⟨ℙ, inferInstance⟩,        φ.toFun <| UB <| Classical.choice <| ProbabilityMeasure.nonempty ⟨ℙ, inferInstance⟩⟩      exact Finset.mem_product.mpr ⟨FiniteRange.mem _ _, FiniteRange.mem _ _⟩    replace hc := Finset.sum_lt_sum_of_nonempty h_nonempty hc    have h_p_one : ∑ x ∈ X ×ˢ Y, p x.1 x.2 = 1 := by      simp_rw [Finset.sum_product, p, mul_div_mul_comm, ← Finset.mul_sum,        ← sum_prob_preimage hA h_φ_AX, sum_prob_preimage hB h_φ_BY, mul_one]    rewrite [← Finset.sum_mul, h_p_one, one_mul, Finset.sum_product] at hc    exact not_le_of_gt hc h_sum  obtain ⟨x, y, hxy⟩ := this  refine ⟨x, y, A_ x.val, B_ y.val, rfl, rfl, .of_subtype, .of_subtype, ?_⟩  rewrite [← inv_div, Real.log_inv]  change _ * -log (p x.val y.val) ≤ M * _  linarith only [hxy]