quasi-borel-spaces/QuasiBorelSpaces/ENNReal.lean at main · YellPika/quasi-borel-spaces · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
module

import QuasiBorelSpaces.Basic
import Mathlib.MeasureTheory.Constructions.BorelSpace.Real
public import QuasiBorelSpaces.Defs
public import QuasiBorelSpaces.OmegaQuasiBorelSpace

public section

namespace QuasiBorelSpace.ENNReal

variable
  {A : Type*} {_ : QuasiBorelSpace A}
  {B : Type*} [Countable B]

@[fun_prop]
lemma isHom_add
    {f : A → ENNReal} (hf : IsHom f)
    {g : A → ENNReal} (hg : IsHom g)
    : IsHom (fun x ↦ f x + g x) := by
  rw [isHom_def] at ⊢ hf hg
  intro φ hφ
  specialize hg hφ
  specialize hf hφ
  simp only [isHom_ofMeasurableSpace] at ⊢ hg hf
  exact Measurable.add hf hg

@[fun_prop]
lemma isHom_mul
    {f : A → ENNReal} (hf : IsHom f)
    {g : A → ENNReal} (hg : IsHom g)
    : IsHom (fun x ↦ f x * g x) := by
  rw [isHom_def] at ⊢ hf hg
  intro φ hφ
  specialize hg hφ
  specialize hf hφ
  simp only [isHom_ofMeasurableSpace] at ⊢ hg hf
  exact Measurable.mul hf hg

@[fun_prop]
lemma isHom_iSup {f : A → B → ENNReal} (hf : ∀ b, IsHom (f · b)) : IsHom fun x ↦ ⨆i, f x i := by
  rw [isHom_def]
  intro φ hφ
  apply isHom_of_measurable
  apply Measurable.iSup fun b ↦ ?_
  apply measurable_of_isHom
  fun_prop

end QuasiBorelSpace.ENNReal

namespace OmegaQuasiBorelSpace.ENNReal

open QuasiBorelSpace

/-- ωQBS structure on `ENNReal` -/
noncomputable instance : OmegaQuasiBorelSpace ENNReal where
  isHom_ωSup := by
    change IsHom fun c : OmegaCompletePartialOrder.Chain ENNReal ↦ ⨆ n, c n
    fun_prop

end OmegaQuasiBorelSpace.ENNReal