type mismatch error

Stream: new members

[Iocta]

1. I can see what it's saying in the first error but I don't know how to fix it.
2. I don't understand the second error

import analysis.normed_space.indicator_function
import measure_theory.set_integral
import analysis.specific_limits
import data.real.basic
import data.nat.basic
import algebra.geom_sum
import tactic.fin_cases
import data.set.basic
import measure_theory.probability_mass_function
import set_theory.cardinal_ordinal


universe u
variables α β : Type u



noncomputable def marginalize1 (f : pmf (α × β)) : pmf β:=
(λb, ∑' a : α, f (a, b))

-- type mismatch, term
--   λ (b : β), ∑' (a : α), ⇑f (a, b)
-- has type
--   β → nnreal
-- but is expected to have type
--   pmf β


noncomputable def marginalize2 (f : pmf (α × β)) : pmf α :=
(λa, ∑' b : β, f (a, b))


def independent (f : pmf (α × β)) : Prop :=
∀ a: α, ∀ b : β, f (a, b) = (marginalize1 f b) * (marginalize2 f a)

-- type mismatch at application
--   marginalize1 f
-- term
--   f
-- has type
--   pmf (α × β) : Type u
-- but is expected to have type
--   Type ? : Type (?+1)

[Alex J. Best]

The type pmf α is { f : α → nnreal // has_sum f 1 } , so to construct a term you need a pair α → nnreal and a proof that the sum is 1, you can write this as a pair with langle rangle.

[Iocta]

Ok that makes sense

[Iocta]

Does that also explain the second error (how)?

[Iocta]

ie

import analysis.normed_space.indicator_function
import measure_theory.set_integral
import analysis.specific_limits
import data.real.basic
import data.nat.basic
import algebra.geom_sum
import tactic.fin_cases
import data.set.basic
import measure_theory.probability_mass_function
import set_theory.cardinal_ordinal


universe u
variables α β : Type u



noncomputable def marginalize1 (f : pmf (α × β)) : pmf β:=
⟨
   (λb, ∑' a : α, f (a, b)),
   begin
    unfold pmf at f,
    cases f,
    sorry,
   end
⟩

#check nhds


noncomputable def marginalize2 (f : pmf (α × β)) : pmf α :=
⟨ (λa, ∑' b : β, f (a, b)), sorry ⟩


def independent (f : pmf (α × β)) : Prop :=
∀ a: α, ∀ b : β, f (a, b) = (marginalize1 f b) * (marginalize2 f a)


-- type mismatch at application
--   marginalize1 f
-- term
--   f
-- has type
--   pmf (α × β) : Type u
-- but is expected to have type
--   Type ? : Type (?+1)

[Alex J. Best]

Did you get the first ones working? I'm not running lean right now so I can't check unfortunately, you might have to add f.val in some places too.

[Alex J. Best]

Oh this is because marginalize1 takes alpha and beta as explicit arguments (try #check marginalize1 to see them).

[Alex J. Best]

So you can change your variables line to variables {α β : Type u} to make them implicit.

[Iocta]

easy fix :-)

[Jeremy Toh]

I am getting a type mismatch error that somehow disappears if I change variable {f : ℕ → ℝ≥0} to variable {f : ℕ → ℝ≥0∞} that I am not sure how to resolve it.

Here is a mwe for more detail:

import Mathlib

open Filter BigOperators ENNReal NNReal Topology Finset

namespace Finset

variable {u : ℕ → ℕ} {f : ℕ → ℝ≥0}

theorem le_sum_schlomilch (hf : ∀ ⦃m n⦄, 0 < m → m ≤ n → f n ≤ f m) (h_pos : ∀ n, 0 < u n)
    (h_u_mono : ∀ ⦃m n⦄, 0 ≤ m → m ≤ n → u m ≤ u n)
    (n : ℕ) :
    (∑ k in range (u n), f k) ≤ ∑ k in range (u 0), f k + ∑ k in range n, (u (k + 1) - u k) • f (u k) := by
    sorry

end Finset

theorem extracted_goal {u : ℕ → ℕ} {f : ℕ → ℝ≥0∞} (hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m)
  (h_pos : ∀ (n : ℕ), 0 < u n) (h_u_mono : ∀ ⦃m n : ℕ⦄, 0 ≤ m → m ≤ n → u m ≤ u n) :
  ⨆ i, ∑ a in range (u i), f a ≤ ∑ k in range (u 0), f k + ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k) := by
  refine' iSup_le fun n => (Finset.le_sum_schlomilch hf h_pos h_u_mono n).trans (add_le_add_left _ _)

Thank you in advance for the help!

[Alex J. Best]

iSup_le requires a complete lattice, and according to

#synth CompleteLattice ℝ≥0∞

#synth CompleteLattice ℝ≥0

NNReal is not one but ENNReal is

[Jeremy Toh]

Ah, I see. Thank you! Is there anyway to fix it without changing it to ℝ≥0∞

[Alex J. Best]

Well you have to think about what you want mathematically, I didn't read it yet in detail, but the crux of the complaint is that in the nonnegative reals we have sequences that tend to infinity and hence have no supremum, when we have an infinity element we are allowed to take sups arbitrarily.
You might want to look at https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/ConditionallyCompleteLattice/Basic.html#ConditionallyCompleteLattice and use somethling like docs#ciSup_le instead?

[Jeremy Toh]

that makes perfect sense! thank you!

[Jeremy Toh]

Is there anyway for me to coerce f : ℕ → ℝ≥0 to f : ℕ → ℝ≥0∞? The error still remains with ciSup_le. If I did not interpret the error message wrongly, I think the problem lies in Lean expecting f to be f : ℕ → ℝ≥0∞but the f in le_sum_schlomilch is f : ℕ → ℝ≥0 instead.

[Alex J. Best]

Maybe we should back up a bit? You have your extracted goal about ℝ≥0∞ and some theorem le_sum_schlomilch which you are changing from ℝ≥0∞ to ℝ≥0 if you can prove schlomilch for ennreal why not use it?

[Alex J. Best]

If you want a function to ennreal from one to nnreal you can use (fun n => f n : ℕ → ℝ≥0∞) but then youll need to prove hf h_pos etc, which should be easy enough but a bit verbose

[Alex J. Best]

And it sounds like you actually want to go the other way? In the extracted goal you have an ennreal valued function but you want to apply a theorem about nnreal valued functions, this isn't a coercion at this point as the function really could equal infinity somewhere

[Jeremy Toh]

Ah you are right. I am actually trying to do the TODO in PSeries as an exercise in learning Lean. Currently, I am trying to adapt the structure of the proof to Schlömilch's. For the original code, it used OrderedAddCommMonoid but it was causing issues with HSub/HSMul/HMul and I took the easy way to use ℝ≥0 instead for now. Maybe I should go back and look at what's the correct algebraic structure to use. Thanks for the help!

[Alex J. Best]

Yeah it sounds like you should stick to NNReal or Real if you can and avoid ENNReal. Good luck with the project it sounds like a good one!