This file contains the definitions and some theorems about t-approximable sets, which are needed in the proof of the Debut Theorem.

def MeasureTheory.𝓚₀ {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] (𝓕 : Filtration T mΩ) (t : T) : Set (Set (T × Ω))

𝓚₀(t) is the collection of subsets of [0, t] × Ω of the form A × C, where A is compact and C is (f t)-measurable.

Equations

• MeasureTheory.𝓚₀ 𝓕 t = {B : Set (T × Ω) | ∃ (K : Set T) (C : Set Ω), B = K ×ˢ C ∧ K ⊆ Set.Iic t ∧ IsCompact K ∧ MeasurableSet C}

@[simp]

theorem MeasureTheory.empty_mem_𝓚₀ {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] (𝓕 : Filtration T mΩ) (t : T) : ∅ ∈ 𝓚₀ 𝓕 t

theorem MeasureTheory.subset_Iic_of_mem_𝓚₀ {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {B : Set (T × Ω)} (hB : B ∈ 𝓚₀ 𝓕 t) : B ⊆ Set.Iic t ×ˢ Set.univ

theorem MeasureTheory.measurableSet_snd_of_mem_𝓚₀ {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {B : Set (T × Ω)} (hB : B ∈ 𝓚₀ 𝓕 t) : MeasurableSet (Prod.snd '' B)

If B ∈ 𝓚₀(t), then its projetion over Ω is (f t)-measurable.

theorem MeasureTheory.inter_mem_𝓚₀ {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] [T2Space T] {𝓕 : Filtration T mΩ} {t : T} {B B' : Set (T × Ω)} (hB : B ∈ 𝓚₀ 𝓕 t) (hB' : B' ∈ 𝓚₀ 𝓕 t) : B ∩ B' ∈ 𝓚₀ 𝓕 t

𝓚₀(t) is closed under intersection.

inductive MeasureTheory.𝓚 {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] (𝓕 : Filtration T mΩ) (t : T) : Set (Set (T × Ω))

𝓚(t) is the collection of finite unions of sets in 𝓚₀(t).

• base {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} (B : Set (T × Ω)) (hB : B ∈ 𝓚₀ 𝓕 t) : 𝓚 𝓕 t B
• union {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} (B B' : Set (T × Ω)) (hB : B ∈ 𝓚 𝓕 t) (hB' : B' ∈ 𝓚 𝓕 t) : 𝓚 𝓕 t (B ∪ B')

theorem MeasureTheory.𝓚₀_subset_𝓚 {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] (𝓕 : Filtration T mΩ) (t : T) : 𝓚₀ 𝓕 t ⊆ 𝓚 𝓕 t

theorem MeasureTheory.mem_𝓚_iff {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] (𝓕 : Filtration T mΩ) (t : T) (B : Set (T × Ω)) : B ∈ 𝓚 𝓕 t ↔ ∃ (s : Finset (Set (T × Ω))), ↑s ⊆ 𝓚₀ 𝓕 t ∧ B = ⋃ x ∈ s, x

@[simp]

theorem MeasureTheory.empty_mem_𝓚 {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} : ∅ ∈ 𝓚 𝓕 t

theorem MeasureTheory.subset_Iic_of_mem_𝓚 {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {B : Set (T × Ω)} (hB : B ∈ 𝓚 𝓕 t) : B ⊆ Set.Iic t ×ˢ Set.univ

theorem MeasureTheory.union_mem_𝓚 {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {f : Filtration T mΩ} {t : T} {B B' : Set (T × Ω)} (hB : B ∈ 𝓚 f t) (hB' : B' ∈ 𝓚 f t) : B ∪ B' ∈ 𝓚 f t

𝓚(t) is closed under union.

theorem MeasureTheory.measurableSet_snd_of_mem_𝓚 {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {B : Set (T × Ω)} (hB : B ∈ 𝓚 𝓕 t) : MeasurableSet (Prod.snd '' B)

If B ∈ 𝓚(t), then its projection over Ω is (f t)-measurable.

theorem MeasureTheory.inter_mem_𝓚 {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] [T2Space T] {f : Filtration T mΩ} {t : T} {B B' : Set (T × Ω)} (hB : B ∈ 𝓚 f t) (hB' : B' ∈ 𝓚 f t) : B ∩ B' ∈ 𝓚 f t

𝓚(t) is closed under intersection.

def MeasureTheory.𝓚δ {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] (𝓕 : Filtration T mΩ) (t : T) : Set (Set (T × Ω))

𝓚δ(t) is the collection of countable intersections of sets in 𝓚(t).

Equations

• MeasureTheory.𝓚δ 𝓕 t = {B : Set (T × Ω) | ∃ ℬ ⊆ MeasureTheory.𝓚 𝓕 t, ℬ.Nonempty ∧ ℬ.Countable ∧ B = ⋂ b ∈ ℬ, b}

theorem MeasureTheory.subset_Iic_of_mem_𝓚δ {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {B : Set (T × Ω)} (hB : B ∈ 𝓚δ 𝓕 t) : B ⊆ Set.Iic t ×ˢ Set.univ

theorem MeasureTheory.𝓚_subset_𝓚δ {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {B : Set (T × Ω)} (hB : B ∈ 𝓚 𝓕 t) : B ∈ 𝓚δ 𝓕 t

𝓚(t) ⊆ 𝓚δ(t).

@[simp]

theorem MeasureTheory.empty_mem_𝓚δ {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} : ∅ ∈ 𝓚δ 𝓕 t

theorem MeasureTheory.union_mem_𝓚δ {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {B B' : Set (T × Ω)} (hB : B ∈ 𝓚δ 𝓕 t) (hB' : B' ∈ 𝓚δ 𝓕 t) : B ∪ B' ∈ 𝓚δ 𝓕 t

𝓚δ(t) is closed under union.

theorem MeasureTheory.inter_mem_𝓚δ {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {B B' : Set (T × Ω)} (hB : B ∈ 𝓚δ 𝓕 t) (hB' : B' ∈ 𝓚δ 𝓕 t) : B ∩ B' ∈ 𝓚δ 𝓕 t

𝓚δ(t) is closed under intersection.

theorem MeasureTheory.iInter_mem_𝓚δ {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {B : ℕ → Set (T × Ω)} (hB : ∀ (n : ℕ), B n ∈ 𝓚δ 𝓕 t) : ⋂ (n : ℕ), B n ∈ 𝓚δ 𝓕 t

𝓚δ(t) is closed under countable intersections.

theorem MeasureTheory.iInf_snd_eq_snd_iInf_of_mem_𝓚δ {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {ℬ : ℕ → Set (T × Ω)} (hℬ : ∀ (i : ℕ), ℬ i ∈ 𝓚δ 𝓕 t) (h_desc : ∀ (i : ℕ), ℬ (i + 1) ⊆ ℬ i) : ⋂ (i : ℕ), Prod.snd '' ℬ i = Prod.snd '' ⋂ (i : ℕ), ℬ i

In 𝓚δ, the projection over Ω and countable descending intersections commute.

theorem MeasureTheory.measurableSet_snd_of_mem_𝓚δ {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} [T2Space T] {B : Set (T × Ω)} (hB : B ∈ 𝓚δ 𝓕 t) : MeasurableSet (Prod.snd '' B)

If B ∈ 𝓚δ(t), then its projetion over Ω is (𝓕 t)-measurable.

def MeasureTheory.𝓛₀ {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] (X : Type u_3) [TopologicalSpace X] (𝓕 : Filtration T mΩ) (t : T) : Set (Set (X × T × Ω))

𝓛₀(X) is the collection of sets of the form A ×ˢ B, where A : Set X is compact and B ∈ 𝓚 𝓕 t.

Equations

• MeasureTheory.𝓛₀ X 𝓕 t = {C : Set (X × T × Ω) | ∃ (A : Set X) (B : Set (T × Ω)), IsCompact A ∧ B ∈ MeasureTheory.𝓚 𝓕 t ∧ A ×ˢ B = C}

inductive MeasureTheory.𝓛₁ {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] (X : Type u_3) [TopologicalSpace X] (𝓕 : Filtration T mΩ) (t : T) : Set (Set (X × T × Ω))

𝓛₁(X) is the collection of finite unions of sets in 𝓛₀(X).

• base {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {X : Type u_3} [TopologicalSpace X] {𝓕 : Filtration T mΩ} {t : T} {L : Set (X × T × Ω)} (hL : L ∈ 𝓛₀ X 𝓕 t) : 𝓛₁ X 𝓕 t L
• union {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {X : Type u_3} [TopologicalSpace X] {𝓕 : Filtration T mΩ} {t : T} {L L' : Set (X × T × Ω)} (hL : L ∈ 𝓛₁ X 𝓕 t) (hL' : L' ∈ 𝓛₁ X 𝓕 t) : 𝓛₁ X 𝓕 t (L ∪ L')

def MeasureTheory.𝓛 {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] (X : Type u_3) [TopologicalSpace X] (𝓕 : Filtration T mΩ) (t : T) : Set (Set (X × T × Ω))

𝓛(X) is the collection of intersections of countable decreasing sequences in 𝓛₁(X).

Equations

• MeasureTheory.𝓛 X 𝓕 t = {B : Set (X × T × Ω) | ∃ (L : ℕ → Set (X × T × Ω)), Antitone L ∧ (∀ (n : ℕ), L n ∈ MeasureTheory.𝓛₁ X 𝓕 t) ∧ B = ⋂ (n : ℕ), L n}

def MeasureTheory.𝓛σ {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] (X : Type u_3) [TopologicalSpace X] (𝓕 : Filtration T mΩ) (t : T) : Set (Set (X × T × Ω))

𝓛σ(X) is the collection of unions of countable increasing sequences in 𝓛(X).

Equations

• MeasureTheory.𝓛σ X 𝓕 t = {B : Set (X × T × Ω) | ∃ (L : ℕ → Set (X × T × Ω)), Monotone L ∧ (∀ (n : ℕ), L n ∈ MeasureTheory.𝓛 X 𝓕 t) ∧ B = ⋃ (n : ℕ), L n}

def MeasureTheory.𝓛σδ {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] (X : Type u_3) [TopologicalSpace X] (𝓕 : Filtration T mΩ) (t : T) : Set (Set (X × T × Ω))

𝓛σδ(X) is the collection of intersections of countable decreasing sequences in 𝓛σ(X).

Equations

• MeasureTheory.𝓛σδ X 𝓕 t = {B : Set (X × T × Ω) | ∃ (L : ℕ → Set (X × T × Ω)), Antitone L ∧ (∀ (n : ℕ), L n ∈ MeasureTheory.𝓛σ X 𝓕 t) ∧ B = ⋂ (n : ℕ), L n}

theorem MeasureTheory.exists_mem_𝓛σδ_of_measurableSet {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {mT : MeasurableSpace T} [BorelSpace T] {A : Set (T × Ω)} (hA_subs : A ⊆ Set.Iic t ×ˢ Set.univ) (hA : MeasurableSet A) : ∃ (X : Type u_3) (x : TopologicalSpace X) (_ : CompactSpace X) (_ : T2Space X), ∃ B ∈ 𝓛σδ X 𝓕 t, A = Prod.snd '' B

If A is measurable with respect to the product sigma algebra of the Borel sigma algebra on T and 𝓕 t, then there exists a compact Hausdorff space X and a set B ∈ 𝓛σδ X 𝓕 t such that A is the projection of B on T × Ω.

structure MeasureTheory.Approximation {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] (𝓕 : Filtration T mΩ) (P : Measure Ω) (t : T) (A : Set (T × Ω)) : Type (max u_1 u_2)

An approximation of A ⊆ Set.Iic t ×ˢ .univ is a sequence of sets B ε ⊆ A for every ε > 0 such that B ε ∈ 𝓚δ 𝓕 t, and the projection of B ε on Ω approximates A in measure as ε tends to 0.

• B : ENNReal → Set (T × Ω)

  The approximating sets.

• A_subset : A ⊆ Set.Iic t ×ˢ Set.univ
• B_mem (ε : ENNReal) : ε > 0 → self.B ε ∈ 𝓚δ 𝓕 t
• B_subset_A (ε : ENNReal) : ε > 0 → self.B ε ⊆ A
• le (ε : ENNReal) : ε > 0 → P (Prod.snd '' A) ≤ P (Prod.snd '' self.B ε) + ε

def MeasureTheory.Approximation.of_mem_𝓚δ {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {A : Set (T × Ω)} (P : Measure Ω) (hA : A ∈ 𝓚δ 𝓕 t) : Approximation 𝓕 P t A

A set A ∈ 𝓚δ(t) is approximable (the approximation is the set itself).

Equations

• MeasureTheory.Approximation.of_mem_𝓚δ P hA = { B := fun (x : ENNReal) => A, A_subset := ⋯, B_mem := ⋯, B_subset_A := ⋯, le := ⋯ }

def MeasureTheory.Approximation.B' {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {P : Measure Ω} {A : Set (T × Ω)} (𝒜 : Approximation 𝓕 P t A) : ℕ → Set (T × Ω)

Given an approximation 𝒜, then 𝒜.B' n is the union of B 1, B (1/2), ..., B (1/n). This gives us an increasing approximating sequence.

Equations

• 𝒜.B' n = ⋃ m ∈ Finset.Icc 1 n, 𝒜.B (1 / ↑m)

@[simp]

theorem MeasureTheory.Approximation.B'_zero {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {P : Measure Ω} {A : Set (T × Ω)} (𝒜 : Approximation 𝓕 P t A) : 𝒜.B' 0 = ∅

theorem MeasureTheory.Approximation.B'_succ {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {P : Measure Ω} {A : Set (T × Ω)} (𝒜 : Approximation 𝓕 P t A) (n : ℕ) : 𝒜.B' (n + 1) = 𝒜.B' n ∪ 𝒜.B (1 / (↑n + 1))

theorem MeasureTheory.Approximation.B_subset_B' {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {P : Measure Ω} {A : Set (T × Ω)} (𝒜 : Approximation 𝓕 P t A) (n : ℕ) [NeZero n] : 𝒜.B (1 / ↑n) ⊆ 𝒜.B' n

theorem MeasureTheory.Approximation.B'_mem {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {P : Measure Ω} {A : Set (T × Ω)} (𝒜 : Approximation 𝓕 P t A) (n : ℕ) : 𝒜.B' n ∈ 𝓚δ 𝓕 t

theorem MeasureTheory.Approximation.B'_subset_A {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {P : Measure Ω} {A : Set (T × Ω)} (𝒜 : Approximation 𝓕 P t A) (n : ℕ) : 𝒜.B' n ⊆ A

theorem MeasureTheory.Approximation.le' {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {P : Measure Ω} {A : Set (T × Ω)} (𝒜 : Approximation 𝓕 P t A) (n : ℕ) : P (Prod.snd '' A) ≤ P (Prod.snd '' 𝒜.B' n) + 1 / ↑n

theorem MeasureTheory.Approximation.B'_mono {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {P : Measure Ω} {A : Set (T × Ω)} (𝒜 : Approximation 𝓕 P t A) : Monotone 𝒜.B'

theorem MeasureTheory.Approximation.measurableSet_snd_iUnion_B' {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {P : Measure Ω} {A : Set (T × Ω)} [T2Space T] (𝒜 : Approximation 𝓕 P t A) : MeasurableSet (Prod.snd '' ⋃ (n : ℕ), 𝒜.B' n)

theorem MeasureTheory.Approximation.measure_snd_iUnion_B' {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {P : Measure Ω} {A : Set (T × Ω)} (𝒜 : Approximation 𝓕 P t A) : P (Prod.snd '' ⋃ (n : ℕ), 𝒜.B' n) = P (Prod.snd '' A)

theorem MeasureTheory.Approximation.measure_snd_diff {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {P : Measure Ω} {A : Set (T × Ω)} [IsFiniteMeasure P] (𝒜 : Approximation 𝓕 P t A) : P (Prod.snd '' A \ Prod.snd '' ⋃ (n : ℕ), 𝒜.B' n) = 0

theorem MeasureTheory.Approximation.measurableSet_snd {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {P : Measure Ω} {A : Set (T × Ω)} [T2Space T] (𝒜 : Approximation 𝓕 P t A) : MeasurableSet (Prod.snd '' A)

If there exists an approximation of A, then the projection of A over Ω is measurable with respect to 𝓕 t.

theorem MeasureTheory.Approximation.tendsto_measure_diff_B' {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {P : Measure Ω} {A : Set (T × Ω)} (𝒜 : Approximation 𝓕 P t A) : Filter.Tendsto (fun (n : ℕ) => P (Prod.snd '' A \ Prod.snd '' 𝒜.B' n)) Filter.atTop (nhds 0)

def MeasureTheory.Approximation.of_mem_prod_borel {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder T] [TopologicalSpace T] {𝓕 : Filtration T mΩ} {t : T} {A : Set (T × Ω)} {mT : MeasurableSpace T} [BorelSpace T] (P : Measure Ω) (hA_subs : A ⊆ Set.Iic t ×ˢ Set.univ) (hA : MeasurableSet A) : Approximation 𝓕 P t A

If A is measurable with respect to the product sigma algebra of the Borel sigma algebra on T and 𝓕 t, then it is approximable.

Equations

• MeasureTheory.Approximation.of_mem_prod_borel P hA_subs hA = { B := sorry, A_subset := ⋯, B_mem := ⋯, B_subset_A := ⋯, le := ⋯ }