equivalence of finite sums and series

Stream: Is there code for X?

[Pietro Lavino]

I a working with different types of sum, and it would be convenient if it was possible to switch from one and the other when I am going for example from a finite sum and I want to consider the series with the same first terms as the finite sum and then rest we are just adding zeros.

[Yaël Dillies]

Do you have a specific statement in mind? That's the first step

[Pietro Lavino]

Yaël Dillies said:

Do you have a specific statement in mind? That's the first step

I have a finite (n terms) partition of a probability space coded as a function. I associate with this function the sum of the measure of each set in partition. I also have a function that extends the finite partition to a countable one so a function with naturals as the domain, by letting the extended domain go to the empty set. Then to consider the corresponding series, which will be identical to the first sum but with an infinite tails of zeroes being added ( the measure of empty set).

[Yaël Dillies]

Great! Now, can you write that statement in Lean? That's the second step

[Pietro Lavino]

Yaël Dillies said:

Great! Now, can you write that statement in Lean? That's the second step

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.Data.ENNReal.Real
import Init.Data.Fin.Basic
import Mathlib.Data.Set.Lattice
import Mathlib.Data.Set.Function
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.Convex.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Ring
import Mathlib.MeasureTheory.Measure.NullMeasurable


open MeasureTheory
open ENNReal
open Set
open Function
open scoped BigOperators
open Finset



structure partition {α : Type*} (m : MeasurableSpace α) (μ : Measure α) [IsProbabilityMeasure μ] :=
  f : ℕ → Set α         -- A function from natural numbers to sets of terms in α
  measurable : ∀ n, MeasurableSet (f n)  -- Each set is measurable
  (disjoint : ∀ i j, i ≠ j → μ (f i ∩ f j) = 0)  -- The sets are pairwise disjoint
  (cover : (⋃ n, f n) = Set.univ)  -- The union of all sets covers the entire space
--defining finite partitions given measure

structure finpart {α : Type*} (m : MeasurableSpace α) (μ : Measure α) [IsProbabilityMeasure μ] (n: ℕ):=
  (f : Fin n → Set α)          -- A function from finite sets of size n to sets of terms in α
  (measurable : ∀ i : Fin n, MeasurableSet (f i))  -- Each set is measurable
  (disjoint : ∀ i j, i ≠ j → μ (f i ∩ f j) = 0)  -- The sets are pairwise disjoint
  (cover : (⋃ i, f i) = Set.univ)  -- The union of all sets covers the entire space

def finpart_to_partition {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
  (n : ℕ) (fp : finpart m μ n) : partition m μ
    where
  f := λ k ↦ if h : k < n then fp.f ⟨k, h⟩ else ∅
  measurable:= by
    intro k; by_cases h : k<n
    · simp only [dif_pos h]
      exact fp.measurable ⟨k, h⟩
    · simp only [dif_neg h]
      exact MeasurableSet.empty
  disjoint:=  by
    intro i j hij
    by_cases hi : i < n
    · by_cases hj: j < n
      · simp only [dif_pos hi, dif_pos hj]
        exact fp.disjoint ⟨i, hi⟩ ⟨j, hj⟩ (λ h ↦ hij (Fin.val_eq_of_eq h))
      · simp only [dif_pos hi, dif_neg hj, Set.inter_empty, measure_empty]
    · simp only [dif_neg hi, Set.empty_inter, measure_empty]
  cover:= by
    ext x
    constructor
    · tauto
    · intro h;dsimp; rw[← fp.cover] at h; rcases mem_iUnion.mp h with ⟨a, ha⟩
      rw[mem_iUnion]
      use a; simp only [dif_pos a.is_lt]; exact ha



theorem  sumeq {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
  (n : ℕ) (fp : finpart m μ n):
  (∑' n', (μ (fp.f n')).toReal)= ∑' n', (μ ((finpart_to_partition n fp).f n')).toReal := by
  have h: ∀ n' ∉ Fin n,  (μ ((finpart_to_partition n fp).f n')).toReal = 0 := by
    sorry

I am trying to use tsum_eq_sum but the issue is that it works when the set from which the finite sum is indexed is of type Finset \N , since \N is the set indexing the infinite sum. Is there a way perhaps to show that sets of type Fin n can be considered (coerced) as sets of type Finset \N. I don't think I should go back and change the definitions of partitions as it is convenient to use Fin n.