simple function sum coercion

Stream: Is there code for X?

[Vasily Ilin]

This lemma feels like it should be in mathlib but I could not find it. I would appreciate a pointer on how to prove it.

import Mathlib.MeasureTheory.Function.SimpleFunc
open MeasureTheory BigOperators
variable [MeasurableSpace Ω]

lemma coe_sum (f : I → (SimpleFunc Ω ℝ)) [Fintype I] : (∑ i, f i).toFun = ∑ i, (f i).toFun := by
  sorry

[Chris Birkbeck]

Is it not something like'Finset.sum_map_val? Here:https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Basic.html#Finset.sum_map_val

[Vasily Ilin]

I don't see any similarity. My lemma is about SimpleFunc

[Chris Birkbeck]

Hmm sorry maybe I misunderstood the question then. I thought you simply wanted to commute the function and sum

[Vasily Ilin]

I edited the question to include the imports. I need to compute the sum and the coercion from SimpleFunc to the underlying function

[Vasily Ilin]

I need docs#MeasureTheory.SimpleFunc.coe_add but instead of two functions, finitely many of them

[Vasily Ilin]

Mathematically, I would do induction on the cardinality of the fintype I. But I'm struggling to make it work in Lean.

[Chris Birkbeck]

Sorry I'm on mobile and not much help, but can you do induction on your finset instead of it's cardinality?

[Vasily Ilin]

I don't know what it would mean to do induction on a finset

[Vasily Ilin]

I tried induction' I with I hI but it gave an error.

[Chris Birkbeck]

Something like this: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Finset/Basic.html#Finset.induction

[Vasily Ilin]

This looks quite relevant. The difficulty becomes translating between a fintype and a finset

[Yaël Dillies]

It would be called SimpleFunc.coe_sum but it is indeed missing. Please state it with ⇑

[Yaël Dillies]

There's no difficulty at all. But you need to generalise your statement

[Vasily Ilin]

I'm sure there is no difficulty for someone skilled at Lean but so far I have not found a way

[Vasily Ilin]

I'm not sure what you mean by stating it with ⇑. You mean instead of toFun? I feel uneasy about the many up arrows that Lean employs so I wanted to be explicit about my coercion.

[Vasily Ilin]

To what should the statement be generalized? I tried

lemma coe_sum : ∀ n : ℕ, ∀ I : Type, ∀(f : I → (SimpleFunc Ω ℝ)),
(hI : Fintype I) → (hn : Fintype.card I = n) → (∑ i, f i).toFun = ∑ i, (f i).toFun

and tried induction on n but got stuck.

[Yaël Dillies]

import Mathlib.MeasureTheory.Function.SimpleFunc

open MeasureTheory BigOperators

namespace SimpleFunc
variable {ι α β : Type*} [MeasurableSpace α] [CommMonoid β]

@[to_additive (attr := simp, norm_cast)]
lemma coe_prod (f : ι → SimpleFunc α β) (s : Finset ι) : ∏ i in s, f i = ∏ i in s, ⇑(f i) := by
  induction s using Finset.cons_induction <;> simp [*]

[Yaël Dillies]

(untested, but it should work)

[Yaël Dillies]

Vasily Ilin said:

I feel uneasy about the many up arrows that Lean employs so I wanted to be explicit about my coercion.

Sadly for you, if f : α →ₛ β, then ⇑f and f.toFun are not syntactically equal, so you really have to stick to the first.

[Yaël Dillies]

Else no lemma will apply, except the one turning f.toFun into ⇑f.

[Vasily Ilin]

I'm getting an error in the →ₛ symbol. I know I can just change it to SimpleFunction \a \b but I assume this code compiles for you. It's weird that it does not compile for me

[Yaël Dillies]

No, I literally wrote it on Zulip without an infoview to look at. I fixed it now.

[Vasily Ilin]

It's very impressive. Thank you for your help

[Chris Birkbeck]

Yaël Dillies said:

(untested, but it should work)

isnt this essentially how LLMs solve IMO problems in lean? guess without an infoview and then check the answer. This is more evidence towards the belief you're just a LLM Yaël :laughing:

[Eric Wieser]

Come on Yael, the canonical proof is obviously to conjure the →+ and use map_sum. As an AI language model, you should know this!