awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
h :
  ∀ (μ : FiniteMeasure Ω),
    Membership.mem (γ := Set (FiniteMeasure Ω)) (range toFiniteMeasure) μ ↔
      Membership.mem (γ := Set (FiniteMeasure Ω)) {μ : FiniteMeasure Ω | μ.mass = 1} μ
⊢ Eq.{u_1 + 1} (α := Set (FiniteMeasure Ω)) (range toFiniteMeasure) {μ : FiniteMeasure Ω | μ.mass = 1}

Tactic:
ext μ
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
h : ∃ (y : ProbabilityMeasure Ω), y.toFiniteMeasure = μ
ν : ProbabilityMeasure Ω
hν : ν.toFiniteMeasure = μ
⊢ μ.mass = 1

Tactic:
simp [← hν]
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
h : ∀ (h : μ.mass = 1), ∃ (y : ProbabilityMeasure Ω), y.toFiniteMeasure = μ
⊢ (∃ (y : ProbabilityMeasure Ω), y.toFiniteMeasure = μ) ↔ μ.mass = 1

Tactic:
refine ⟨fun ⟨ν, hν⟩ ↦ by simp [← hν], fun h ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
h : μ.mass = 1
⊢ (↑μ : Measure Ω).real univ = 1

Tactic:
simpa using h
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
h : μ.mass = 1
h₁ : toFiniteMeasure (Subtype.mk (p := fun (μ : Measure Ω) ↦ IsProbabilityMeasure μ) (↑μ : Measure Ω) ⋯) = μ
⊢ ∃ (y : ProbabilityMeasure Ω), y.toFiniteMeasure = μ

Tactic:
refine ⟨⟨μ, isProbabilityMeasure_iff_real.2 (by simpa using h)⟩, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
h : μ.mass = 1
h₁ :
  ∀ (s : Set Ω) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      (((↑(toFiniteMeasure (Subtype.mk (p := fun (μ : Measure Ω) ↦ IsProbabilityMeasure μ) (↑μ : Measure Ω) ⋯)) :
              Measure Ω) :
            (a : Set Ω) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
⊢ toFiniteMeasure (Subtype.mk (p := fun (μ : Measure Ω) ↦ IsProbabilityMeasure μ) (↑μ : Measure Ω) ⋯) = μ

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
h : μ.mass = 1
s : Set Ω
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (((↑(toFiniteMeasure (Subtype.mk (p := fun (μ : Measure Ω) ↦ IsProbabilityMeasure μ) (↑μ : Measure Ω) ⋯)) :
            Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
⊢ μ.toFiniteMeasure ≠ 0

Tactic:
simp [← FiniteMeasure.mass_nonzero_iff]

Premises used: MeasureTheory.FiniteMeasure.mass_nonzero_iff
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
this :
  Eq.{u_1 + 1} (α := Set (Measure Ω)) {μ : Measure Ω | IsProbabilityMeasure μ}
    (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) {1})
rw :
  MeasurableSet.{u_1} (α := Measure Ω) (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) {1})
⊢ MeasurableSet.{u_1} (α := Measure Ω) {μ : Measure Ω | IsProbabilityMeasure μ}

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
this :
  Eq.{u_1 + 1} (α := Set (Measure Ω)) {μ : Measure Ω | IsProbabilityMeasure μ}
    (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) {1})
⊢ MeasurableSet.{u_1} (α := Measure Ω) (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) {1})

Tactic:
Measure.measurable_coe MeasurableSet.univ (measurableSet_singleton 1)

Premises used: MeasureTheory.Measure.measurable_coe, MeasurableSingletonClass.measurableSet_singleton, OfNat.ofNat, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
this :
  Eq.{u_1 + 1} (α := Set (Measure Ω)) {μ : Measure Ω | IsProbabilityMeasure μ}
    (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) {1})
⊢ MeasurableSet.{u_1} (α := Measure Ω) (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) {1})

Tactic:
exact Measure.measurable_coe MeasurableSet.univ (measurableSet_singleton 1)

Premises used: MeasureTheory.Measure.measurable_coe, MeasurableSingletonClass.measurableSet_singleton, OfNat.ofNat, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
suffices :
  Eq.{u_1 + 1} (α := Set (Measure Ω)) {μ : Measure Ω | IsProbabilityMeasure μ}
    (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) {1})
⊢ MeasurableSet.{u_1} (α := Measure Ω) {μ : Measure Ω | IsProbabilityMeasure μ}

Tactic:
suffices { μ : Measure Ω | IsProbabilityMeasure μ } = (fun μ => μ univ) ⁻¹' {1} by
    rw [this]
    exact Measure.measurable_coe MeasurableSet.univ (measurableSet_singleton 1)
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
h :
  ∀ (x : Measure Ω),
    Membership.mem (γ := Set (Measure Ω)) {μ : Measure Ω | IsProbabilityMeasure μ} x ↔
      Membership.mem (γ := Set (Measure Ω))
        (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) {1}) x
⊢ Eq.{u_1 + 1} (α := Set (Measure Ω)) {μ : Measure Ω | IsProbabilityMeasure μ}
    (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) {1})

Tactic:
ext _
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
x : Measure Ω
⊢ Membership.mem (γ := Set (Measure Ω)) {μ : Measure Ω | IsProbabilityMeasure μ} x ↔
    Membership.mem (γ := Set (Measure Ω))
      (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) {1}) x

Tactic:
apply isProbabilityMeasure_iff

Premises used: MeasureTheory.isProbabilityMeasure_iff
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
apply :
  ∀ (s : Set (α × β)),
    Membership.mem (γ := Set (Set (α × β)))
        (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
        s →
      Measurable (β := ℝ≥0∞) fun (a : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
        ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) s
⊢ Measurable (β := Measure (α × β)) fun (μ : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
    (↑μ.1 : Measure α).prod (↑μ.2 : Measure β)

Tactic:
apply Measurable.measure_of_isPiSystem_of_isProbabilityMeasure generateFrom_prod.symm
    isPiSystem_prod _

Premises used: isPiSystem_prod, generateFrom_prod, Eq.symm, Measurable.measure_of_isPiSystem_of_isProbabilityMeasure
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
simp :
  ∀ (s : Set (α × β)) (x : Set α),
    MeasurableSet x →
      ∀ (x_1 : Set β),
        MeasurableSet x_1 →
          x ×ˢ x_1 = s →
            Measurable (β := ℝ≥0∞) fun (a : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
              ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) s
⊢ ∀ (s : Set (α × β)),
    Membership.mem (γ := Set (Set (α × β)))
        (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
        s →
      Measurable (β := ℝ≥0∞) fun (a : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
        ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) s

Tactic:
simp only [mem_image2, mem_setOf_eq, forall_exists_index, and_imp]

Premises used: and_imp, Set.mem_image2, forall_exists_index, Set.mem_setOf_eq
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
s : Set (α × β)
u : Set α
Hu : MeasurableSet u
v : Set β
Hv : MeasurableSet v
Heq : u ×ˢ v = s
simp_rw :
  Measurable (β := ℝ≥0∞) fun (a : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (a : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
    ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) s

Tactic:
simp_rw [← Heq, Measure.prod_prod]

Premises used: MeasureTheory.Measure.prod_prod
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
s : Set (α × β)
u : Set α
Hu : MeasurableSet u
v : Set β
Hv : MeasurableSet v
Heq : u ×ˢ v = s
hf :
  Measurable (β := ℝ≥0∞) fun (a : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
    ((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u
hg :
  Measurable (β := ℝ≥0∞) fun (a : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
    ((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v
⊢ Measurable (β := ℝ≥0∞) fun (a : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v : ℝ≥0∞)

Tactic:
apply Measurable.mul

Premises used: Measurable.mul
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
s : Set (α × β)
u : Set α
Hu : MeasurableSet u
v : Set β
Hv : MeasurableSet v
Heq : u ×ˢ v = s
⊢ Measurable (β := ℝ≥0∞) fun (a : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
    ((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u

Tactic:
(Measure.measurable_coe Hu).comp (measurable_subtype_coe.comp measurable_fst)

Premises used: measurable_subtype_coe, MeasureTheory.Measure.measurable_coe, Measurable.comp, measurable_fst
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
s : Set (α × β)
u : Set α
Hu : MeasurableSet u
v : Set β
Hv : MeasurableSet v
Heq : u ×ˢ v = s
⊢ Measurable (β := ℝ≥0∞) fun (a : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
    ((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u

Tactic:
exact (Measure.measurable_coe Hu).comp (measurable_subtype_coe.comp measurable_fst)

Premises used: measurable_subtype_coe, MeasureTheory.Measure.measurable_coe, Measurable.comp, measurable_fst
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
s : Set (α × β)
u : Set α
Hu : MeasurableSet u
v : Set β
Hv : MeasurableSet v
Heq : u ×ˢ v = s
⊢ Measurable (β := ℝ≥0∞) fun (a : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
    ((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v

Tactic:
(Measure.measurable_coe Hv).comp (measurable_subtype_coe.comp measurable_snd)

Premises used: measurable_subtype_coe, MeasureTheory.Measure.measurable_coe, Measurable.comp, measurable_snd
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
s : Set (α × β)
u : Set α
Hu : MeasurableSet u
v : Set β
Hv : MeasurableSet v
Heq : u ×ˢ v = s
⊢ Measurable (β := ℝ≥0∞) fun (a : Prod.{u_2, u_3} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
    ((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v

Tactic:
exact (Measure.measurable_coe Hv).comp (measurable_subtype_coe.comp measurable_snd)

Premises used: measurable_subtype_coe, MeasureTheory.Measure.measurable_coe, Measurable.comp, measurable_snd
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
f : ℕ → Set Ω
hf : Summable (α := ℝ≥0) fun (n : ℕ) ↦ (μ : (a : Set Ω) → ℝ≥0) (f n)
⊢ LE.le (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) (⋃ (n : ℕ), f n) : ℝ≥0) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0) (f n) : ℝ≥0)

Tactic:
simpa [← ENNReal.coe_le_coe, ENNReal.coe_tsum hf] using MeasureTheory.measure_iUnion_le f

Premises used: ENNReal.coe_tsum, ENNReal.coe_le_coe, MeasureTheory.measure_iUnion_le
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
⊢ LipschitzWith (β := ℝ≥0) 1 fun (f : Ω →ᵇ ℝ≥0) ↦ μ.toFiniteMeasure.testAgainstNN f

Tactic:
μ.mass_toFiniteMeasure ▸ μ.toFiniteMeasure.testAgainstNN_lipschitz

Premises used: MeasureTheory.ProbabilityMeasure.mass_toFiniteMeasure, Eq.rec, MeasureTheory.ProbabilityMeasure.toFiniteMeasure, MeasureTheory.FiniteMeasure.testAgainstNN_lipschitz
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
⊢ Continuous[instTopologicalSpace, FiniteMeasure.instTopologicalSpace] toFiniteMeasure

Tactic:
continuous_induced_dom

Premises used: continuous_induced_dom
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
⊢ Eq (α := (a : Ω →ᵇ ℝ≥0) → ℝ≥0) (⇑μ.toWeakDualBCNN : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) μ.toFiniteMeasure.testAgainstNN

Tactic:
rfl

Premises used: ENNReal.toNNReal, MeasureTheory.FiniteMeasure.testAgainstNN, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
f : Ω →ᵇ ℝ≥0
⊢ ((μ.toWeakDualBCNN : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f =
    (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toNNReal

Tactic:
rfl

Premises used: MeasureTheory.ProbabilityMeasure, ENNReal.toNNReal, MeasureTheory.FiniteMeasure.testAgainstNN, WithTop.untopD, MeasureTheory.ProbabilityMeasure.toMeasure, WithTop.recTopCoe, rfl
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
⊢ Continuous[instTopologicalSpace, _] fun (μ : ProbabilityMeasure Ω) ↦ μ.toWeakDualBCNN

Tactic:
FiniteMeasure.toWeakDualBCNN_continuous.comp toFiniteMeasure_continuous

Premises used: MeasureTheory.ProbabilityMeasure.toWeakDualBCNN, Continuous.comp, MeasureTheory.FiniteMeasure.toWeakDualBCNN_continuous, MeasureTheory.ProbabilityMeasure.toFiniteMeasure_continuous
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ Continuous[instTopologicalSpace, _] fun (μ : ProbabilityMeasure Ω) ↦ μ.toFiniteMeasure.testAgainstNN f

Tactic:
(FiniteMeasure.continuous_testAgainstNN_eval f).comp toFiniteMeasure_continuous

Premises used: MeasureTheory.FiniteMeasure.continuous_testAgainstNN_eval, Continuous.comp, ENNReal.toNNReal, MeasureTheory.FiniteMeasure.testAgainstNN, WithTop.untopD, MeasureTheory.ProbabilityMeasure.toFiniteMeasure_continuous, WithTop.recTopCoe
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
⊢ _root_.R1Space.{u_1} (ProbabilityMeasure Ω)

Tactic:
(toFiniteMeasure_isEmbedding Ω).r1Space

Premises used: Topology.IsInducing.r1Space, Topology.IsEmbedding.toIsInducing, MeasureTheory.ProbabilityMeasure.toFiniteMeasure_isEmbedding
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
δ : Type u_2
F : Filter δ
μs : δ → ProbabilityMeasure Ω
μ₀ : ProbabilityMeasure Ω
⊢ Tendsto μs F (𝓝 μ₀) ↔ Tendsto (toFiniteMeasure ∘ μs) F (𝓝 μ₀.toFiniteMeasure)

Tactic:
(toFiniteMeasure_isEmbedding Ω).tendsto_nhds_iff

Premises used: Topology.IsEmbedding.tendsto_nhds_iff, MeasureTheory.ProbabilityMeasure.toFiniteMeasure_isEmbedding
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
rw :
  Tendsto (toFiniteMeasure ∘ μs) F (𝓝 μ.toFiniteMeasure) ↔
    ∀ (f : Ω →ᵇ ℝ≥0),
      Tendsto (fun (i : γ) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
⊢ Tendsto μs F (𝓝 μ) ↔
    ∀ (f : Ω →ᵇ ℝ≥0),
      Tendsto (fun (i : γ) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)))

Tactic:
rw [tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds]

Premises used: MeasureTheory.ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ Tendsto (toFiniteMeasure ∘ μs) F (𝓝 μ.toFiniteMeasure) ↔
    ∀ (f : Ω →ᵇ ℝ≥0),
      Tendsto (fun (i : γ) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)))

Tactic:
FiniteMeasure.tendsto_iff_forall_lintegral_tendsto

Premises used: MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto, MeasureTheory.ProbabilityMeasure, MeasureTheory.ProbabilityMeasure.toMeasure
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ Tendsto (toFiniteMeasure ∘ μs) F (𝓝 μ.toFiniteMeasure) ↔
    ∀ (f : Ω →ᵇ ℝ≥0),
      Tendsto (fun (i : γ) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)))

Tactic:
exact FiniteMeasure.tendsto_iff_forall_lintegral_tendsto

Premises used: MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ Tendsto μs F (𝓝 μ) ↔
    ∀ (f : Ω →ᵇ ℝ),
      Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑μ : Measure Ω)))

Tactic:
simp [tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds,
    FiniteMeasure.tendsto_iff_forall_integral_tendsto]

Premises used: MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_tendsto, MeasureTheory.ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst_3 : RCLike 𝕜
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ Tendsto μs F (𝓝 μ) ↔
    ∀ (f : Ω →ᵇ 𝕜),
      Tendsto.{u_2, u_3} (β := 𝕜) (fun (i : γ) ↦ ∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑μ : Measure Ω)))

Tactic:
simp [tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds,
    FiniteMeasure.tendsto_iff_forall_integral_rclike_tendsto 𝕜]

Premises used: MeasureTheory.ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds, MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_rclike_tendsto
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
X : Type u_2
inst_3 : TopologicalSpace X
μs : X → ProbabilityMeasure Ω
⊢ Continuous[inst_3, instTopologicalSpace] μs ↔
    ∀ (f : Ω →ᵇ ℝ≥0),
      Continuous[inst_3, _] fun (x : X) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(μs x) : Measure Ω)

Tactic:
simp [continuous_iff_continuousAt, ContinuousAt, tendsto_iff_forall_lintegral_tendsto,
    forall_comm (α := X)]

Premises used: ContinuousAt, forall_comm, continuous_iff_continuousAt, MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
X : Type u_2
inst_3 : TopologicalSpace X
μs : X → ProbabilityMeasure Ω
⊢ Continuous[inst_3, instTopologicalSpace] μs ↔
    ∀ (f : Ω →ᵇ ℝ), Continuous[inst_3, _] fun (x : X) ↦ ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(μs x) : Measure Ω)

Tactic:
simp [continuous_iff_continuousAt, ContinuousAt, tendsto_iff_forall_integral_tendsto,
    forall_comm (α := X)]

Premises used: ContinuousAt, forall_comm, continuous_iff_continuousAt, MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_tendsto
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
⊢ Continuous[instTopologicalSpace, _] fun (μ : ProbabilityMeasure X) ↦
    ∫⁻ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure X)

Tactic:
continuous_iff_forall_continuous_lintegral.1 continuous_id _

Premises used: MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuous_lintegral, continuous_id, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
f : X →ᵇ ℝ
⊢ Continuous[instTopologicalSpace, _] fun (μ : ProbabilityMeasure X) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂(↑μ : Measure X)

Tactic:
continuous_iff_forall_continuous_integral.1 continuous_id _

Premises used: continuous_id, Iff.mp, MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuous_integral
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
X : Type u_2
inst_3 : TopologicalSpace X
μs : X → ProbabilityMeasure Ω
inst_4 : CompactSpace Ω
⊢ Continuous[inst_3, instTopologicalSpace] μs ↔
    ∀ (f : C(Ω, ℝ≥0)),
      Continuous[inst_3, _] fun (x : X) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(μs x) : Measure Ω)

Tactic:
continuous_iff_forall_continuous_lintegral.trans
    (ContinuousMap.equivBoundedOfCompact ..).symm.forall_congr_left

Premises used: ContinuousMap.equivBoundedOfCompact, Equiv.forall_congr_left, MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuous_lintegral, Iff.trans, Equiv.symm
-- Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
X : Type u_2
inst_3 : TopologicalSpace X
μs : X → ProbabilityMeasure Ω
inst_4 : CompactSpace Ω
⊢ Continuous[inst_3, instTopologicalSpace] μs ↔
    ∀ (f : C(Ω, ℝ)), Continuous[inst_3, _] fun (x : X) ↦ ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(μs x) : Measure Ω)

Tactic:
continuous_iff_forall_continuous_integral.trans
    (ContinuousMap.equivBoundedOfCompact ..).symm.forall_congr_left

Premises used: ContinuousMap.equivBoundedOfCompact, Equiv.forall_congr_left, MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuous_integral, Iff.trans, Equiv.symm