convert the index set of the summation into an assumption?

Stream: lean4

[Yifan Bai]

Excuse me~ This is my first time using zulip, seeking for some help :face_holding_back_tears:
How to convert the index set of the summation into a hypothesis?

def φ_sum (t : Set E) (ht : t.Finite) (φ : (x : E) → x ∈ ht.toFinset → ℝ → ℝ) :=
  ∑ x ∈ ht.toFinset, φ x _

Here the position of the placeholder needs the assumption x ∈ ht.toFinset, how to achieve this?

[Ruben Van de Velde]

Probably ht.toFinset.attach

[Etienne Marion]

I don't know how to do exactly this, but let me give you two different ways to write it which I think are more idiomatic.

The first one is to use a function which is defined everywhere, event if out of the set you're interested in you put a junk value:

import Mathlib

variable {E : Type*}

noncomputable def φ_sum (t : Set E) (ht : t.Finite) (φ : E → ℝ → ℝ) :=
  ∑ x ∈ ht.toFinset, φ x

The second way is to consider a function whose domain is the set you're interested in, namely something like φ : ht.toFinset → ℝ → ℝ. This works because ht.toFinset will automatically be considered as a type, and an element x : ht.toFinset is a pair whose first component is the underlying element in E, and the second one is a proof that this element is in ht.toFinset. Those can be obtained via x.1 : E and x.2 : x.1 ∈ ht.toFinset. If you use such a function you can directly write a sum indexed by the type ht.toFinset:

import Mathlib

variable {E : Type*}

noncomputable def φ_sum (t : Set E) (ht : t.Finite) (φ : ht.toFinset → ℝ → ℝ) :=
  ∑ x : ht.toFinset, φ x

The noncomputable is just here to tell Lean that you're definition needs some classical reasoning to be defined.

[Moritz Firsching]

you could also consider using ∑'

noncomputable def φ_sum (t : Set E) (ht : t.Finite) (g : (x : E) → x ∈ ht.toFinset → ℝ → ℝ) :=
   ∑' x : t, g x (by aesop)

[Yifan Bai]

Etienne Marion said:

I don't know how to do exactly this, but let me give you two different ways to write it which I think are more idiomatic.

The first one is to use a function which is defined everywhere, event if out of the set you're interested in you put a junk value:

import Mathlib

variable {E : Type*}

noncomputable def φ_sum (t : Set E) (ht : t.Finite) (φ : E → ℝ → ℝ) :=
  ∑ x ∈ ht.toFinset, φ x

The second way is to consider a function whose domain is the set you're interested in, namely something like φ : ht.toFinset → ℝ → ℝ. This works because ht.toFinset will automatically be considered as a type, and an element x : ht.toFinset is a pair whose first component is the underlying element in E, and the second one is a proof that this element is in ht.toFinset. Those can be obtained via x.1 : E and x.2 : x.1 ∈ ht.toFinset. If you use such a function you can directly write a sum indexed by the type ht.toFinset:

import Mathlib

variable {E : Type*}

noncomputable def φ_sum (t : Set E) (ht : t.Finite) (φ : ht.toFinset → ℝ → ℝ) :=
  ∑ x : ht.toFinset, φ x

The noncomputable is just here to tell Lean that you're definition needs some classical reasoning to be defined.

Yeah if the type is like this then it will be convenient, but here I get $\phi$ by such a theorem: ∀ x ∈ t.toFinset, ∃ η ∈ ℝ, ∃ φ ∈ A η, ..., where $A$ is a set of function. I use choose to get $\eta$ and $\phi$, then the type of $\eta$ will be (x : E) → x ∈ t.toFinset → ℝ automatically, and the type of $\phi$ will be (x : E) → x ∈ t.toFinset → ℝ → ℝ..

[Yifan Bai]

Moritz Firsching said:

you could also consider using ∑'

noncomputable def φ_sum (t : Set E) (ht : t.Finite) (g : (x : E) → x ∈ ht.toFinset → ℝ → ℝ) :=
   ∑' x : t, g x (by aesop)

This method truly works, thank you very much! :saluting_face:

[Etienne Marion]

What you want to do in that case is rather to use the tactic choose!, which will get rid of the dependency

[Yifan Bai]

@Etienne Marion Thank you! It's amazing, this is what I really needs, thank you very much!