ofENat

Stream: new members

[Niclas Kupper]

I am trying to cast a variable of type ℝ≥0∞ to type ℕ∞, but the right coercion does not seem to exist. Am I missing something? For more context I want to create a point measure:

structure PointMeasure (α : Type*) [MeasurableSpace α] extends Measure α where
  measureEnatOf : Set α → ℕ∞
  coeMeasureEnatOf : ∀ s, measureOf s = ENNReal.ofENat (measureEnatOf s)

but there is no ofENat

[Notification Bot]

A message was moved here from #new members > Showing group operation is closed on a subset. by Eric Wieser.

[Eric Wieser]

Can you use ofNNReal?

[Niclas Kupper]

Thanks for moving the message! ofNNReal also does not seem to exist.

[Eric Wieser]

~It's called docs#ENNReal.some, but should probably be renamed~ Edit: now it exists, docs#ENNReal.ofNNReal

[Eric Wieser]

Can you make your question a #mwe by adding imports?

[Niclas Kupper]

This also doesn't work :( ENNReal.some is from ℝ≥0 to ℝ≥0∞. I need from ℕ∞ to ℝ≥0∞.

[Niclas Kupper]

There is a workaround by handling the infinity case seperately, but it's kinda ugly.

[Eric Wieser]

Ah you're right, I wasn't paying attention

[Yakov Pechersky]

WithTop.map (fun n : Nat => (n : NNReal))

?

[Eric Wieser]

That would work as an implementation, but is going to have defeq issues unles you wrap it in an API

[Eric Wieser]

Eric Wieser said:

It's called docs#ENNReal.some, but should probably be renamed

#8276

[Niclas Kupper]

I am now having a very similar issue. How Can I map a function of type Set \alpha -> \nat to Set \alpha -> \enat? I have already tried using WithTop.map or WithTop.some, but could not get those to work. For context:

structure PointMeasure (α : Type*) [MeasurableSpace α] extends Measure α where
  measureEnatOf : Set α → ℕ∞
  coeMeasureEnatOf : ∀ s, measureOf s = WithTop.map (fun n : ℕ => (n : ℝ≥0)) (measureEnatOf s)

structure FinitePointMeasure (α : Type*) [MeasurableSpace α] extends Measure α where
  measureNatOf : Set α → ℕ
  coeMeasureNatOf : ∀ s, measureOf s = (fun n : ℕ => (n : ℝ≥0)) (measureNatOf s)

lemma FinitePointMeasure_is_PointMeasure {α : Type*} [MeasurableSpace α]
  (μ : FinitePointMeasure α) : PointMeasure α :=
  {
    toOuterMeasure := μ.toOuterMeasure
    m_iUnion := μ.m_iUnion
    trimmed := μ.trimmed
    measureEnatOf := ???
  }

[Eric Wieser]

Can you make that a #mwe?

[Yakov Pechersky]

That's not a lemma, should be a def, I think. Because measures are data. measureEnatOf s := mu.measureNatOf s
That lets the Nat to ENat coercion take care of it

[Yakov Pechersky]

Haven't tested it

[Yakov Pechersky]

Also, (\u) \comp mu.measureNatOf could work, for pointfree style

[Niclas Kupper]

I got it now, or, at least Lean4 is happy. I guess its not clear yet if these are the best definitions:

structure PointMeasure (α : Type*) [MeasurableSpace α] extends Measure α where
  measureEnatOf : Set α → ℕ∞
  coeMeasureEnatOf : ∀ s, measureOf s = WithTop.map (fun n : ℕ => (n : ℝ≥0)) (measureEnatOf s)

structure FinitePointMeasure (α : Type*) [MeasurableSpace α] extends Measure α where
  measureNatOf : Set α → ℕ
  coeMeasureNatOf : ∀ s, measureOf s = (fun n : ℕ => (n : ℝ≥0)) (measureNatOf s)

lemma FinitePointMeasure_is_PointMeasure {α : Type*} [MeasurableSpace α]
  (μ : FinitePointMeasure α) : PointMeasure α :=
  {
    toOuterMeasure := μ.toOuterMeasure
    m_iUnion := μ.m_iUnion
    trimmed := μ.trimmed
    measureEnatOf :=  (↑) ∘ μ.measureNatOf
    coeMeasureEnatOf := by
      intro s
      rw [μ.coeMeasureNatOf]
      rfl
  }

[Eric Wieser]

Sorry to sound like a stuck record, but please make this a #mwe!

[Eric Wieser]

It's still missing imports and open commands