awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.CentralLimitTheorem
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] ≠ 0
⊢ HasLaw (fun (ω : Ω') ↦ Y ω / √Var[X 0; P])
    (gaussianReal (0 / √Var[X 0; P]) (Var[X 0; P].toNNReal / NNReal.mk (HPow.hPow (β := ℕ) (√Var[X 0; P]) 2) ⋯)) P'

Tactic:
gaussianReal_div_const hY _

Premises used: ProbabilityTheory.gaussianReal_div_const
-- Module: Mathlib.Probability.CentralLimitTheorem
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] ≠ 0
h₁ : 0 = 0 / √Var[X 0; P]
h₂ : 1 = Var[X 0; P].toNNReal / NNReal.mk (HPow.hPow (β := ℕ) (√Var[X 0; P]) 2) ⋯
⊢ HasLaw (fun (ω : Ω') ↦ Y ω / √Var[X 0; P]) (gaussianReal 0 1) P'

Tactic:
convert! gaussianReal_div_const hY _

Premises used: ProbabilityTheory.gaussianReal_div_const
-- Module: Mathlib.Probability.CentralLimitTheorem
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] ≠ 0
⊢ 0 = 0 / √Var[X 0; P]

Tactic:
simp
-- Module: Mathlib.Probability.CentralLimitTheorem
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] ≠ 0
h₁ : (↑1 : ℝ) = (↑(Var[X 0; P].toNNReal / NNReal.mk (HPow.hPow (β := ℕ) (√Var[X 0; P]) 2) ⋯) : ℝ)
⊢ 1 = Var[X 0; P].toNNReal / NNReal.mk (HPow.hPow (β := ℕ) (√Var[X 0; P]) 2) ⋯

Tactic:
ext
-- Module: Mathlib.Probability.CentralLimitTheorem
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] ≠ 0
⊢ (↑1 : ℝ) = (↑(Var[X 0; P].toNNReal / NNReal.mk (HPow.hPow (β := ℕ) (√Var[X 0; P]) 2) ⋯) : ℝ)

Tactic:
simp [h]
-- Module: Mathlib.Probability.CentralLimitTheorem
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] ≠ 0
⊢ HasLaw (fun (ω : Ω') ↦ Y ω / √Var[X 0; P]) (gaussianReal 0 1) P'

Tactic:
have : HasLaw (fun ω ↦ Y ω / √Var[X 0; P]) (gaussianReal 0 1) P' := by
    convert! gaussianReal_div_const hY _
    · simp
    · ext; simp [h]
-- Module: Mathlib.Probability.CentralLimitTheorem
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] ≠ 0
this : HasLaw (fun (ω : Ω') ↦ Y ω / √Var[X 0; P]) (gaussianReal 0 1) P'
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ √Var[X 0; P] * x

Tactic:
fun_prop
-- Module: Mathlib.Probability.CentralLimitTheorem
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] ≠ 0
this : HasLaw (fun (ω : Ω') ↦ Y ω / √Var[X 0; P]) (gaussianReal 0 1) P'
h₁ :
  ∀ (x : ℕ) (x_1 : Ω),
    (√(↑x : ℝ))⁻¹ * (∑ k ∈ Finset.range x, X k x_1 - HMul.hMul (α := ℝ) (↑x : ℝ) (∫ (x : Ω), X 0 x ∂P)) =
      ((fun (x : ℝ) ↦ √Var[X 0; P] * x) ∘ fun (ω : Ω) ↦
          (√((↑x : ℝ) * Var[X 0; P]))⁻¹ *
            (∑ k ∈ Finset.range x, X k ω - HMul.hMul (α := ℝ) (↑x : ℝ) (∫ (x : Ω), X 0 x ∂P)))
        x_1
h₂ : Y = (fun (x : ℝ) ↦ √Var[X 0; P] * x) ∘ fun (ω : Ω') ↦ Y ω / √Var[X 0; P]
⊢ TendstoInDistribution (Ω := fun (n : ℕ) ↦ Ω) (m := fun (i : ℕ) ↦ mΩ) (mE := Real.measurableSpace)
    (fun (n : ℕ) (ω : Ω) ↦
      (√(↑n : ℝ))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P)))
    atTop Y (fun (x : ℕ) ↦ P) P'

Tactic:
convert!
    (tendstoInDistribution_inv_sqrt_mul_var_mul_sum_sub this h hindep hident).continuous_comp (g :=
      (√Var[X 0; P] * ·)) (by fun_prop)

Premises used: _private.0.ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_var_mul_sum_sub, MeasureTheory.TendstoInDistribution.continuous_comp
-- Module: Mathlib.Probability.CentralLimitTheorem
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] ≠ 0
this : HasLaw (fun (ω : Ω') ↦ Y ω / √Var[X 0; P]) (gaussianReal 0 1) P'
x : ℕ
x_1 : Ω
h₁ :
  (∑ k ∈ Finset.range x, X k x_1 - HMul.hMul (α := ℝ) (↑x : ℝ) (∫ (x : Ω), X 0 x ∂P)) / √(↑x : ℝ) =
    (∑ k ∈ Finset.range x, X k x_1 - HMul.hMul (α := ℝ) (↑x : ℝ) (∫ (x : Ω), X 0 x ∂P)) * √Var[X 0; P] /
      (√(↑x : ℝ) * √Var[X 0; P])
⊢ (√(↑x : ℝ))⁻¹ * (∑ k ∈ Finset.range x, X k x_1 - HMul.hMul (α := ℝ) (↑x : ℝ) (∫ (x : Ω), X 0 x ∂P)) =
    ((fun (x : ℝ) ↦ √Var[X 0; P] * x) ∘ fun (ω : Ω) ↦
        (√((↑x : ℝ) * Var[X 0; P]))⁻¹ *
          (∑ k ∈ Finset.range x, X k ω - HMul.hMul (α := ℝ) (↑x : ℝ) (∫ (x : Ω), X 0 x ∂P)))
      x_1

Tactic:
simp [field]
-- Module: Mathlib.Probability.CentralLimitTheorem
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] ≠ 0
this : HasLaw (fun (ω : Ω') ↦ Y ω / √Var[X 0; P]) (gaussianReal 0 1) P'
x : ℕ
x_1 : Ω
⊢ (∑ k ∈ Finset.range x, X k x_1 - HMul.hMul (α := ℝ) (↑x : ℝ) (∫ (x : Ω), X 0 x ∂P)) / √(↑x : ℝ) =
    (∑ k ∈ Finset.range x, X k x_1 - HMul.hMul (α := ℝ) (↑x : ℝ) (∫ (x : Ω), X 0 x ∂P)) * √Var[X 0; P] /
      (√(↑x : ℝ) * √Var[X 0; P])

Tactic:
field_simp [h]
-- Module: Mathlib.Probability.CentralLimitTheorem
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] ≠ 0
this : HasLaw (fun (ω : Ω') ↦ Y ω / √Var[X 0; P]) (gaussianReal 0 1) P'
h₁ : ∀ (x : Ω'), Y x = ((fun (x : ℝ) ↦ √Var[X 0; P] * x) ∘ fun (ω : Ω') ↦ Y ω / √Var[X 0; P]) x
⊢ Y = (fun (x : ℝ) ↦ √Var[X 0; P] * x) ∘ fun (ω : Ω') ↦ Y ω / √Var[X 0; P]

Tactic:
ext
-- Module: Mathlib.Probability.CentralLimitTheorem
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] ≠ 0
this : HasLaw (fun (ω : Ω') ↦ Y ω / √Var[X 0; P]) (gaussianReal 0 1) P'
x : Ω'
h₁ : Y x = Y x * √Var[X 0; P] / √Var[X 0; P]
⊢ Y x = ((fun (x : ℝ) ↦ √Var[X 0; P] * x) ∘ fun (ω : Ω') ↦ Y ω / √Var[X 0; P]) x

Tactic:
simp [field]
-- Module: Mathlib.Probability.CentralLimitTheorem
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] ≠ 0
this : HasLaw (fun (ω : Ω') ↦ Y ω / √Var[X 0; P]) (gaussianReal 0 1) P'
x : Ω'
⊢ Y x = Y x * √Var[X 0; P] / √Var[X 0; P]

Tactic:
field_simp [h]
-- Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
Goal:
V : Type u_1
p : (↑I : Type)
inst : Countable V
S : Set (SimpleGraph V)
rw :
  Eq (α := ENNReal)
    (((comap edgeSet setBer(Sym2.diagSetᶜ, p) : Measure (SimpleGraph V)) : (a : Set (SimpleGraph V)) → ENNReal) S :
      ENNReal)
    (((setBer(Sym2.diagSetᶜ, p) : Measure (Set (Sym2 V))) : (a : Set (Set (Sym2 V))) → ENNReal) (edgeSet '' S) :
      ENNReal)
rw₁ rw₂ :
  Eq (α := ENNReal)
    (((setBer(Sym2.diagSetᶜ, p) : Measure (Set (Sym2 V))) : (a : Set (Set (Sym2 V))) → ENNReal) (edgeSet '' S) :
      ENNReal)
    (((setBer(Sym2.diagSetᶜ, p) : Measure (Set (Sym2 V))) : (a : Set (Set (Sym2 V))) → ENNReal) (edgeSet '' S) :
      ENNReal)
⊢ Eq (α := ENNReal) ((G(V, p) : (a : Set (SimpleGraph V)) → ENNReal) S : ENNReal)
    (((setBer(Sym2.diagSetᶜ, p) : Measure (Set (Sym2 V))) : (a : Set (Set (Sym2 V))) → ENNReal) (edgeSet '' S) :
      ENNReal)

Tactic:
rw [binomialRandom, measurableEmbedding_edgeSet.comap_apply]

Premises used: SimpleGraph.binomialRandom, MeasurableEmbedding.comap_apply, SimpleGraph.measurableEmbedding_edgeSet
-- Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
Goal:
V : Type u_1
p : (↑I : Type)
inst : Countable V
S : Set (SimpleGraph V)
⊢ Eq (α := ENNReal) ((G(V, p) : (a : Set (SimpleGraph V)) → ENNReal) S : ENNReal)
    (((infinitePi (X := fun (e : Sym2 V) ↦ Prop) fun (e : Sym2 V) ↦
              HSMul.hSMul (β := Measure Prop) (toNNReal p) (dirac ¬e.IsDiag) +
                HSMul.hSMul (β := Measure Prop) (toNNReal (σ p)) (dirac False) :
            Measure ((i : Sym2 V) → Prop)) :
          (a : Set ((i : Sym2 V) → Prop)) → ENNReal)
        ((fun (G : SimpleGraph V) (e : Sym2 V) ↦ e ∈ G.edgeSet) '' S) :
      ENNReal)

Tactic:
simp [binomialRandom_apply', setBernoulli_apply, ← Set.image_comp]

Premises used: SimpleGraph.binomialRandom_apply', Set.image_comp, ProbabilityTheory.setBernoulli_apply
-- Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
Goal:
V : Type u_1
p : (↑I : Type)
inst : Countable V
⊢ IsProbabilityMeasure G(V, p)

Tactic:
measurableEmbedding_edgeSet.isProbabilityMeasure_comap ?_

Premises used: SimpleGraph.binomialRandom, SimpleGraph.measurableEmbedding_edgeSet, MeasurableEmbedding.isProbabilityMeasure_comap
-- Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
Goal:
V : Type u_1
p : (↑I : Type)
inst : Countable V
refine : ∀ᵐ (a : Set (Sym2 V)) ∂setBer(Sym2.diagSetᶜ, p), Membership.mem (γ := Set (Set (Sym2 V))) (Set.range edgeSet) a
⊢ IsProbabilityMeasure G(V, p)

Tactic:
refine measurableEmbedding_edgeSet.isProbabilityMeasure_comap ?_

Premises used: SimpleGraph.measurableEmbedding_edgeSet, MeasurableEmbedding.isProbabilityMeasure_comap
-- Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
Goal:
V : Type u_1
p : (↑I : Type)
inst : Countable V
h : ∀ (s : Set (Sym2 V)) (hs : s ⊆ Sym2.diagSetᶜ), Membership.mem (γ := Set (Set (Sym2 V))) (Set.range edgeSet) s
⊢ ∀ᵐ (a : Set (Sym2 V)) ∂setBer(Sym2.diagSetᶜ, p), Membership.mem (γ := Set (Set (Sym2 V))) (Set.range edgeSet) a

Tactic:
filter_upwards [setBernoulli_ae_subset] with s hs

Premises used: ProbabilityTheory.setBernoulli_ae_subset
-- Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
Goal:
V : Type u_1
p : (↑I : Type)
inst : Countable V
s : Set (Sym2 V)
hs : s ⊆ Sym2.diagSetᶜ
⊢ Membership.mem (γ := Set (Set (Sym2 V))) (Set.range edgeSet) s

Tactic:
⟨.fromEdgeSet s, ?_⟩

Premises used: Set.Mem, SimpleGraph.fromEdgeSet, setOf, Exists.intro, Set.range
-- Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
Goal:
V : Type u_1
p : (↑I : Type)
inst : Countable V
s : Set (Sym2 V)
hs : s ⊆ Sym2.diagSetᶜ
h : (fromEdgeSet s).edgeSet = s
⊢ Membership.mem (γ := Set (Set (Sym2 V))) (Set.range edgeSet) s

Tactic:
refine ⟨.fromEdgeSet s, ?_⟩
-- Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
Goal:
V : Type u_1
p : (↑I : Type)
inst : Countable V
s : Set (Sym2 V)
hs : s ⊆ Sym2.diagSetᶜ
⊢ (fromEdgeSet s).edgeSet = s

Tactic:
simpa [← Set.disjoint_compl_right_iff_subset, ← Set.compl_setOf] using hs

Premises used: Set.disjoint_compl_right_iff_subset, Set.compl_setOf
-- Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
Goal:
V : Type u_1
inst : Countable V
⊢ G(V, 0) = dirac ⊥

Tactic:
simp [binomialRandom_eq_map]

Premises used: SimpleGraph.binomialRandom_eq_map
-- Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
Goal:
V : Type u_1
inst : Countable V
⊢ G(V, 1) = dirac ⊤

Tactic:
simp [binomialRandom_eq_map]

Premises used: SimpleGraph.binomialRandom_eq_map
-- Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
Goal:
V : Type u_1
p : (↑I : Type)
inst : Finite V
G : SimpleGraph V
intro :
  ∀ (val : Fintype V),
    (G(V, p) : (a : Set (SimpleGraph V)) → ENNReal) {G} =
      (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
        (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
⊢ (G(V, p) : (a : Set (SimpleGraph V)) → ENNReal) {G} =
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
      (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)

Tactic:
cases nonempty_fintype V

Premises used: nonempty_fintype
-- Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
Goal:
V : Type u_1
p : (↑I : Type)
inst : Finite V
G : SimpleGraph V
val : Fintype V
intro :
  (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard * (↑(toNNReal (σ p)) : ENNReal) ^ (Sym2.diagSetᶜ \ G.edgeSet).ncard =
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
      (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
⊢ (G(V, p) : (a : Set (SimpleGraph V)) → ENNReal) {G} =
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
      (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)

Tactic:
simp only [binomialRandom, measurableEmbedding_edgeSet.comap_apply, Set.image_singleton,
    edgeSet_subset_compl_diagSet, setBernoulli_singleton, Set.toFinite]

Premises used: Set.image_singleton, ProbabilityTheory.setBernoulli_singleton, SimpleGraph.binomialRandom, Set.toFinite, MeasurableEmbedding.comap_apply, SimpleGraph.measurableEmbedding_edgeSet, SimpleGraph.edgeSet_subset_compl_diagSet
-- Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
Goal:
V : Type u_1
p : (↑I : Type)
inst : Finite V
G : SimpleGraph V
val : Fintype V
⊢ G.edgeSet ⊆ Sym2.diagSetᶜ

Tactic:
simp
-- Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
Goal:
V : Type u_1
p : (↑I : Type)
inst : Finite V
G : SimpleGraph V
val : Fintype V
intro :
  (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
      (↑(toNNReal (σ p)) : ENNReal) ^ (Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ - G.edgeSet.ncard) =
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
      (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
⊢ (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard * (↑(toNNReal (σ p)) : ENNReal) ^ (Sym2.diagSetᶜ \ G.edgeSet).ncard =
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
      (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)

Tactic:
rw [Set.ncard_diff (by simp)]

Premises used: Set.ncard_diff
-- Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
Goal:
V : Type u_1
p : (↑I : Type)
inst : Finite V
G : SimpleGraph V
val : Fintype V
intro : Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ = (Nat.card V).choose 2
⊢ (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
      (↑(toNNReal (σ p)) : ENNReal) ^ (Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ - G.edgeSet.ncard) =
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
      (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)

Tactic:
congr!
-- Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
Goal:
V : Type u_1
p : (↑I : Type)
inst : Finite V
G : SimpleGraph V
val : Fintype V
intro : Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ = (Fintype.card V).choose 2
intro₁ : Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ = Fintype.card.{u_1} (↑Sym2.diagSetᶜ : Type u_1)
intro₂ : Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ = Nat.card.{u_1} (↑Sym2.diagSetᶜ : Type u_1)
intro₃ intro₄ : Nat.card.{u_1} (↑Sym2.diagSetᶜ : Type u_1) = Nat.card.{u_1} (↑Sym2.diagSetᶜ : Type u_1)
⊢ Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ = (Nat.card V).choose 2

Tactic:
rw [Nat.card_eq_fintype_card, ← Sym2.card_diagSet_compl, Fintype.card_eq_nat_card,
    ← Nat.card_coe_set_eq]

Premises used: Nat.card_coe_set_eq, Sym2.card_diagSet_compl, Fintype.card_eq_nat_card, Nat.card_eq_fintype_card
-- Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
Goal:
V : Type u_1
p : (↑I : Type)
inst : Finite V
G : SimpleGraph V
intro :
  ∀ (val : Fintype V),
    (G(V, p) : (a : Set (SimpleGraph V)) → ENNReal) {G} =
      (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
        (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
intro₁ :
  ∀ (val : Fintype V),
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard * (↑(toNNReal (σ p)) : ENNReal) ^ (Sym2.diagSetᶜ \ G.edgeSet).ncard =
      (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
        (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
intro₂ :
  ∀ (val : Fintype V),
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
        (↑(toNNReal (σ p)) : ENNReal) ^ (Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ - G.edgeSet.ncard) =
      (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
        (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
intro₃ : ∀ (val : Fintype V), Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ = (Nat.card V).choose 2
⊢ (G(V, p) : (a : Set (SimpleGraph V)) → ENNReal) {G} =
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
      (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)

Tactic:
classical
  cases nonempty_fintype V
  simp only [binomialRandom, measurableEmbedding_edgeSet.comap_apply, Set.image_singleton,
    edgeSet_subset_compl_diagSet, setBernoulli_singleton, Set.toFinite]
  rw [Set.ncard_diff (by simp)]
  congr!
  rw [Nat.card_eq_fintype_card, ← Sym2.card_diagSet_compl, Fintype.card_eq_nat_card,
    ← Nat.card_coe_set_eq]

Premises used: Set.image_singleton, ProbabilityTheory.setBernoulli_singleton, SimpleGraph.binomialRandom, Nat.card_coe_set_eq, Sym2.card_diagSet_compl, Set.toFinite, nonempty_fintype, MeasurableEmbedding.comap_apply, SimpleGraph.measurableEmbedding_edgeSet, Set.ncard_diff, SimpleGraph.edgeSet_subset_compl_diagSet, Fintype.card_eq_nat_card, Nat.card_eq_fintype_card
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : ¬m ≤ m₀
rw : μ[HPow.hPow (β := ℕ) (X - μ[X | m]) 2 | m] = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := Ω → ℝ) 0 0
⊢ Var[X; μ | m] = 0

Tactic:
rw [condVar, condExp_of_not_le hm]

Premises used: MeasureTheory.condExp_of_not_le, ProbabilityTheory.condVar
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
hm : m ≤ m₀
X : Ω → ℝ
μ : Measure Ω
hμm : ¬SigmaFinite (μ.trim hm)
rw : μ[HPow.hPow (β := ℕ) (X - μ[X | m]) 2 | m] = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := Ω → ℝ) 0 0
⊢ Var[X; μ | m] = 0

Tactic:
rw [condVar, condExp_of_not_sigmaFinite hm hμm]

Premises used: MeasureTheory.condExp_of_not_sigmaFinite, ProbabilityTheory.condVar
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
hm : m ≤ m₀
X : Ω → ℝ
μ : Measure Ω
inst : SigmaFinite (μ.trim hm)
⊢ Var[X; μ | m] =
    if Integrable (ε := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - μ[X | m] ω) 2) μ then
      if StronglyMeasurable (β := ℝ) fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - μ[X | m] ω) 2 then fun (ω : Ω) ↦
        HPow.hPow (β := ℕ) (X ω - μ[X | m] ω) 2
      else
        AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ)
          (↑(↑(condExpL1 hm μ fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - μ[X | m] ω) 2) : Ω →ₘ[μ] ℝ) : Ω → ℝ) ⋯
    else 0

Tactic:
condExp_of_sigmaFinite _

Premises used: MeasureTheory.condExp_of_sigmaFinite, ProbabilityTheory.condVar
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
hm : m ≤ m₀
X : Ω → ℝ
μ : Measure Ω
inst : SigmaFinite (μ.trim hm)
hX : StronglyMeasurable X
hXint : Integrable (HPow.hPow (β := ℕ) (X - μ[X | m]) 2) μ
⊢ Var[X; μ | m] = fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - μ[X | m] ω) 2

Tactic:
condExp_of_stronglyMeasurable _ ((hX.sub stronglyMeasurable_condExp).pow _) hXint

Premises used: MeasureTheory.StronglyMeasurable.sub, MeasureTheory.condExp_of_stronglyMeasurable, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.StronglyMeasurable.pow, ProbabilityTheory.condVar
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hXint : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - μ[X | m] ω) 2) μ
⊢ Var[X; μ | m] = 0

Tactic:
condExp_of_not_integrable hXint

Premises used: MeasureTheory.condExp_of_not_integrable, ProbabilityTheory.condVar
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
⊢ Var[0; μ | m] = 0

Tactic:
simp [condVar]

Premises used: ProbabilityTheory.condVar
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
c : ℝ
inl : Var[fun (x : Ω) ↦ 0; μ | m] = 0
inr : ∀ (hc : c ≠ 0), Var[fun (x : Ω) ↦ c; μ | m] = 0
⊢ Var[fun (x : Ω) ↦ c; μ | m] = 0

Tactic:
obtain rfl | hc := eq_or_ne c 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
⊢ Var[fun (x : Ω) ↦ 0; μ | m] = 0

Tactic:
simp [← Pi.zero_def]

Premises used: Pi.zero_def
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
c : ℝ
hc : c ≠ 0
pos : ∀ (hμm : IsFiniteMeasure μ), Var[fun (x : Ω) ↦ c; μ | m] = 0
neg : ∀ (hμm : ¬IsFiniteMeasure μ), Var[fun (x : Ω) ↦ c; μ | m] = 0
⊢ Var[fun (x : Ω) ↦ c; μ | m] = 0

Tactic:
by_cases hμm : IsFiniteMeasure μ

Premises used: MeasureTheory.IsFiniteMeasure
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
c : ℝ
hc : c ≠ 0
hμm : IsFiniteMeasure μ
⊢ Var[fun (x : Ω) ↦ c; μ | m] = 0

Tactic:
simp [condVar, hm]

Premises used: ProbabilityTheory.condVar