how can i extract the set a and b

Stream: new members

[Pietro Lavino]

I am trying to build this function without being in tactic mode

import Mathlib.Topology.Instances.Real
import Mathlib.Analysis.NormedSpace.FiniteDimension
import Mathlib.Analysis.Convolution
import Mathlib.MeasureTheory.Function.Jacobian
import Mathlib.MeasureTheory.Integral.Bochner
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Log.ENNReal
import Mathlib.Data.ENNReal.Real
import Init.Data.Fin.Basic
import Mathlib.Data.Set.Lattice
import Mathlib.Data.Set.Function
import Mathlib.Analysis.Convex.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Ring
import Mathlib.MeasureTheory.Measure.NullMeasurable
import Mathlib.SetTheory.Cardinal.Basic



open MeasureTheory ENNReal Set Function BigOperators Finset



structure partition {α : Type*} (m : MeasurableSpace α) (μ : Measure α) [IsProbabilityMeasure μ] :=
  P : Set (Set α)        -- A function from natural numbers to sets of terms in α
  measurable : ∀ a ∈ P, MeasurableSet a  -- Each set is measurable
  disjoint : ∀ a b : P, a≠b → μ (a ∩ b)=0  -- The sets are pairwise disjoint
  cover : μ (⋃₀ P)ᶜ  = 0  -- The union of all sets covers the entire space
  countable : P.Countable -- at most countable or finite



def injective_function {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
  (p1 p2 : partition m μ)(f:p1.P → ℕ)(g:p2.P → ℕ) : {x | ∃ a b, a ∈ p1.P ∧ b ∈ p2.P ∧ x = a ∩ b} → ℕ :=
  λ x ↦ (Nat.pairEquiv.toFun (f x.2,g x.1))

[Johan Commelin]

But you are already not in tactic mode, right?

[Pietro Lavino]

Johan Commelin said:

But you are already not in tactic mode, right?
yeah i am not, but it is not working as of now

[Johan Commelin]

@Pietro Lavino Can you describe in words what you want to accomplish? You are currently trying to define a function out of a subset. Experience has shown us that in formalization this is often not the optimal path.

[Pietro Lavino]

Johan Commelin said:

Pietro Lavino Can you describe in words what you want to accomplish? You are currently trying to define a function out of a subset. Experience has shown us that in formalization this is often not the optimal path.

The bigger view is am trying to formalize measure theoretic entropy and I am currently restarting from a different definition of partition as a set of sets, i am now trying to define the refinement of two partition which is represented by that set. the function i am trying to build would be an injective function from that set to the naturals to prove that it is a countable set given that the two original partitions are countable. The function should take a set in this set and extract the two sets of which it is the intersection and map those two to the corresponding natural numbers given by injective function from two original partitions to the natural to be composed with a bijection between N*N and N. so given a point in the set i must be able to extract from the existential quantifier the sets a in p1.P and b in p2.P so that i can send x to (Nat.pairEquiv.toFun (f a,g b)).

import Mathlib.Topology.Instances.Real
import Mathlib.Analysis.NormedSpace.FiniteDimension
import Mathlib.Analysis.Convolution
import Mathlib.MeasureTheory.Function.Jacobian
import Mathlib.MeasureTheory.Integral.Bochner
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Log.ENNReal
import Mathlib.Data.ENNReal.Real
import Init.Data.Fin.Basic
import Mathlib.Data.Set.Lattice
import Mathlib.Data.Set.Function
import Mathlib.Analysis.Convex.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Ring
import Mathlib.MeasureTheory.Measure.NullMeasurable
import Mathlib.SetTheory.Cardinal.Basic



open MeasureTheory ENNReal Set Function BigOperators Finset



structure partition {α : Type*} (m : MeasurableSpace α) (μ : Measure α) [IsProbabilityMeasure μ] :=
  P : Set (Set α)        -- A function from natural numbers to sets of terms in α
  measurable : ∀ a ∈ P, MeasurableSet a  -- Each set is measurable
  disjoint : ∀ a b : P, a≠b → μ (a ∩ b)=0  -- The sets are pairwise disjoint
  cover : μ (⋃₀ P)ᶜ  = 0  -- The union of all sets covers the entire space
  countable : P.Countable -- at most countable or finite



def injective_function {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
  (p1 p2 : partition m μ)(f:p1.P → ℕ)(g:p2.P → ℕ) : {x | ∃ a b, a ∈ p1.P ∧ b ∈ p2.P ∧ x = a ∩ b} → ℕ :=
  λ x ↦ (Nat.pairEquiv.toFun (f a,g b))

def refine_partition {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
  (p1 p2 : partition m μ) : partition m μ
    where
  P := {x | ∃ a b, a ∈ p1.P ∧ b ∈ p2.P ∧ x = a ∩ b}
  measurable := by
    intro k hk; dsimp at hk; rcases hk with ⟨a,b,h₁,h₂,h₃⟩;rw[h₃]
    exact MeasurableSet.inter (p1.measurable a h₁) (p2.measurable b h₂)
  disjoint := by
    intro a b hab; dsimp at a b; have h₁:= a; have h₂:= b; have h₃:= hab
    rcases a with ⟨c,d,e,hd,he,hc⟩
    rcases b with ⟨f,g,h,hg,hh,hf⟩
    have : d ≠ g ∨ e ≠ h := by
      by_contra h'; push_neg at h'
      rw [h'.1,h'.2,← hf] at hc; dsimp at hab
      simp at hab
      exact hab hc
    simp
    cases' this with h₁ h₁
    · rw[hc,hf,← Set.inter_assoc,Set.inter_assoc d e g,Set.inter_comm e g,← Set.inter_assoc d g e,Set.inter_assoc]
      let d' : p1.P := ⟨d, hd⟩
      let g' : p1.P := ⟨g, hg⟩
      have :d' ≠ g':= by
        exact Subtype.coe_ne_coe.mp h₁
      have := p1.disjoint d' g' this
      have :μ ( d ∩ g)=0:= by
        exact this
      exact  measure_inter_null_of_null_left (e∩h) this
    · rw[hc,hf,inter_comm g h,← Set.inter_assoc,inter_assoc d e h,inter_comm d,inter_assoc (e ∩ h)]
      let e' : p2.P := ⟨e, he⟩
      let h' : p2.P := ⟨h, hh⟩
      have :e' ≠ h':= by
        exact Subtype.coe_ne_coe.mp h₁
      have := p2.disjoint e' h' this
      have :μ ( e ∩ h)=0:= by
        exact this
      exact measure_inter_null_of_null_left (d∩g) this
  cover := by
    have h: ⋃₀ p1.P ∩ ⋃₀ p2.P  ⊆ ⋃₀ {x | ∃ a b, a ∈ p1.P ∧ b ∈ p2.P ∧ x = a ∩ b} := by
      intro x ⟨hx₁,hx₂⟩;rw [mem_sUnion] at *
      rcases hx₁ with ⟨a,ha₁,ha₂⟩; rcases hx₂ with ⟨b,hb₁,hb₂⟩
      use a∩b;simp; refine ⟨?_, ha₂ ,hb₂⟩
      exact ⟨a,ha₁,b,hb₁,rfl⟩
    have h₁: μ  (⋃₀ p1.P ∩ ⋃₀ p2.P)ᶜ = 0 := by
      rw [Set.compl_inter]
      have h₁ := measure_union_le (μ := μ) ((⋃₀ p1.P)ᶜ) ((⋃₀ p2.P)ᶜ)
      have h₂ :  μ (⋃₀ p1.P)ᶜ + μ (⋃₀ p2.P)ᶜ = 0 := by
        simp only [p1.cover,p2.cover]; rw [add_zero]
    exact measure_mono_null (compl_subset_compl_of_subset h) h₁
  countable := by
    have h₁ := Set.countable_iff_exists_injective.mp p1.countable
    have h₂ := Set.countable_iff_exists_injective.mp p2.countable
    rcases h₁ with ⟨f,hf⟩;rcases h₂ with ⟨g,hg⟩
    have h₆: 2+2 = 4 := by
      linarith
    have h₃: (λ x : {x | ∃ a b, a ∈ p1.P ∧ b ∈ p2.P ∧ x = a ∩ b} ↦ (Nat.pairEquiv.toFun (f ⟨x.1, _⟩,g ⟨x.1,_⟩ ))).Injective := by
      apply?

[Johan Commelin]

Got it. Side remark: you need to assume that f and g are injective, I guess.

I wouldn't be surprised if there are some helper lemmas that allow you to prove that the refinement is countable without building this function. Let me go on a hunt.

[Johan Commelin]

@Pietro Lavino Voila

  countable := by
    have := p1.countable.prod p2.countable
    have := this.image (fun x => x.1 ∩ x.2)
    convert this using 1
    ext x
    simp
    tauto

[Johan Commelin]

I made some small tweaks to the rest of the file. Feel free to use them:

import Mathlib

open MeasureTheory ENNReal Set Function BigOperators

structure partition {α : Type*} (m : MeasurableSpace α) (μ : Measure α) [IsProbabilityMeasure μ] :=
  P : Set (Set α)        -- A function from natural numbers to sets of terms in α
  measurable : ∀ a ∈ P, MeasurableSet a  -- Each set is measurable
  disjoint : ∀ a b : P, a≠b → μ (a ∩ b)=0  -- The sets are pairwise disjoint
  cover : μ (⋃₀ P)ᶜ  = 0  -- The union of all sets covers the entire space
  countable : P.Countable -- at most countable or finite



/- def injective_function {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ] -/
/-   (p1 p2 : partition m μ)(f:p1.P → ℕ)(g:p2.P → ℕ) : {x | ∃ a b, a ∈ p1.P ∧ b ∈ p2.P ∧ x = a ∩ b} → ℕ := -/
/-   λ x ↦ (Nat.pairEquiv.toFun (f a,g b)) -/

def refine_partition {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
  (p1 p2 : partition m μ) : partition m μ
    where
  P := {a ∩ b | (a ∈ p1.P) (b ∈ p2.P)}
  measurable := by
    intro k hk; dsimp at hk; rcases hk with ⟨a, ha, b, hb, rfl⟩
    exact MeasurableSet.inter (p1.measurable a ha) (p2.measurable b hb)
  disjoint := by
    intro a b hab; dsimp at a b; have h₁:= a; have h₂:= b; have h₃:= hab
    rcases a with ⟨c, d, hd, e, he, rfl⟩
    rcases b with ⟨f, g, hg, h, hh, rfl⟩
    have : d ≠ g ∨ e ≠ h := by
      contrapose! hab
      rcases hab with ⟨rfl, rfl⟩
      rfl
    simp
    cases' this with h₁ h₁
    · rw[← inter_assoc, inter_assoc d e g, inter_comm e g, ← inter_assoc d g e, inter_assoc]
      let d' : p1.P := ⟨d, hd⟩
      let g' : p1.P := ⟨g, hg⟩
      have :d' ≠ g':= by
        exact Subtype.coe_ne_coe.mp h₁
      have := p1.disjoint d' g' this
      have :μ ( d ∩ g)=0:= by
        exact this
      exact  measure_inter_null_of_null_left (e∩h) this
    · rw[inter_comm g h, ← inter_assoc, inter_assoc d e h, inter_comm d, inter_assoc (e ∩ h)]
      let e' : p2.P := ⟨e, he⟩
      let h' : p2.P := ⟨h, hh⟩
      have :e' ≠ h':= by
        exact Subtype.coe_ne_coe.mp h₁
      have := p2.disjoint e' h' this
      have :μ ( e ∩ h)=0:= by
        exact this
      exact measure_inter_null_of_null_left (d∩g) this
  cover := by
    have h: ⋃₀ p1.P ∩ ⋃₀ p2.P  ⊆ ⋃₀ {a ∩ b | (a ∈ p1.P) (b ∈ p2.P)} := by
      intro x ⟨hx₁, hx₂⟩;rw [mem_sUnion] at *
      rcases hx₁ with ⟨a, ha₁, ha₂⟩; rcases hx₂ with ⟨b, hb₁, hb₂⟩
      use a∩b;simp; refine ⟨?_, ha₂, hb₂⟩
      exact ⟨a, ha₁, b, hb₁, rfl⟩
    have h₁: μ  (⋃₀ p1.P ∩ ⋃₀ p2.P)ᶜ = 0 := by
      rw [Set.compl_inter]
      have h₁ := measure_union_le (μ := μ) ((⋃₀ p1.P)ᶜ) ((⋃₀ p2.P)ᶜ)
      have h₂ :  μ (⋃₀ p1.P)ᶜ + μ (⋃₀ p2.P)ᶜ = 0 := by
        simp only [p1.cover, p2.cover]; rw [add_zero]
      refine le_antisymm (h₁.trans h₂.le) (by positivity)
    exact measure_mono_null (compl_subset_compl_of_subset h) h₁
  countable := by
    convert (p1.countable.prod p2.countable).image (fun x => x.1 ∩ x.2) using 1
    ext x
    simp
    tauto

[Sébastien Gouëzel]

Note that it would probably be a good idea to define the join of a finite number of partitions (i.e., partitions indexed by a fintype), and then specialize it to get the join of two partitions. You can certainly do it the other way around (for two partitions like you did and then an induction), but I expect that the direct definition will be nicer to work with.

[Pietro Lavino]

Johan Commelin said:

Got it. Side remark: you need to assume that f and g are injective, I guess.

I wouldn't be surprised if there are some helper lemmas that allow you to prove that the refinement is countable without building this function. Let me go on a hunt.

Thanks!