internlm/Lean-Github huggingface dataset:
Theorem: MProd.mk.arg_fstsnd.revDerivUpdate_rule
Proof state before:
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (revDerivUpdate K fun w => { fst := f w, snd := g w }) = fun w =>
    let xdf' := revDerivUpdate K f w;
    let ydg' := revDerivUpdate K g w;
    ({ fst := xdf'.1, snd := ydg'.1 }, fun dxy dw => xdf'.2 dxy.fst (ydg'.2 dxy.snd dw))
Tactic:
unfold revDerivUpdate
Proof state after:
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (fun x =>
      let ydf := revDeriv K (fun w => { fst := f w, snd := g w }) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    fun w =>
    let xdf' :=
      let ydf := revDeriv K f w;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    let ydg' :=
      let ydf := revDeriv K g w;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    ({ fst := xdf'.1, snd := ydg'.1 }, fun dxy dw => xdf'.2 dxy.fst (ydg'.2 dxy.snd dw))
Theorem: MProd.mk.arg_fstsnd.revDerivUpdate_rule
Proof state before:
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (fun x =>
      let ydf := revDeriv K (fun w => { fst := f w, snd := g w }) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    fun w =>
    let xdf' :=
      let ydf := revDeriv K f w;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    let ydg' :=
      let ydf := revDeriv K g w;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    ({ fst := xdf'.1, snd := ydg'.1 }, fun dxy dw => xdf'.2 dxy.fst (ydg'.2 dxy.snd dw))
Tactic:
fun_trans
Proof state after:
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (fun x =>
      ({ fst := f x, snd := g x }, fun dy dx =>
        dx + ((revDeriv K (fun w => f w) x).2 dy.fst + (revDeriv K (fun w => g w) x).2 dy.snd))) =
    fun w => ({ fst := f w, snd := g w }, fun dxy dw => dw + (revDeriv K g w).2 dxy.snd + (revDeriv K f w).2 dxy.fst)
Theorem: MProd.mk.arg_fstsnd.revDerivUpdate_rule
Proof state before:
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (fun x =>
      ({ fst := f x, snd := g x }, fun dy dx =>
        dx + ((revDeriv K (fun w => f w) x).2 dy.fst + (revDeriv K (fun w => g w) x).2 dy.snd))) =
    fun w => ({ fst := f w, snd := g w }, fun dxy dw => dw + (revDeriv K g w).2 dxy.snd + (revDeriv K f w).2 dxy.fst)
Tactic:
funext x
Proof state after:
case h
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : W
⊢ ({ fst := f x, snd := g x }, fun dy dx =>
      dx + ((revDeriv K (fun w => f w) x).2 dy.fst + (revDeriv K (fun w => g w) x).2 dy.snd)) =
    ({ fst := f x, snd := g x }, fun dxy dw => dw + (revDeriv K g x).2 dxy.snd + (revDeriv K f x).2 dxy.fst)
Theorem: MProd.mk.arg_fstsnd.revDerivUpdate_rule
Proof state before:
case h
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : W
⊢ ({ fst := f x, snd := g x }, fun dy dx =>
      dx + ((revDeriv K (fun w => f w) x).2 dy.fst + (revDeriv K (fun w => g w) x).2 dy.snd)) =
    ({ fst := f x, snd := g x }, fun dxy dw => dw + (revDeriv K g x).2 dxy.snd + (revDeriv K f x).2 dxy.fst)
Tactic:
simp
Proof state after:
case h
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : W
⊢ (fun dy dx => dx + ((revDeriv K (fun w => f w) x).2 dy.fst + (revDeriv K (fun w => g w) x).2 dy.snd)) = fun dxy dw =>
    dw + (revDeriv K g x).2 dxy.snd + (revDeriv K f x).2 dxy.fst
Theorem: MProd.mk.arg_fstsnd.revDerivUpdate_rule
Proof state before:
case h
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : W
⊢ (fun dy dx => dx + ((revDeriv K (fun w => f w) x).2 dy.fst + (revDeriv K (fun w => g w) x).2 dy.snd)) = fun dxy dw =>
    dw + (revDeriv K g x).2 dxy.snd + (revDeriv K f x).2 dxy.fst
Tactic:
funext dy dx
Proof state after:
case h.h.h
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : W
dy : MProd X Y
dx : W
⊢ dx + ((revDeriv K (fun w => f w) x).2 dy.fst + (revDeriv K (fun w => g w) x).2 dy.snd) =
    dx + (revDeriv K g x).2 dy.snd + (revDeriv K f x).2 dy.fst
Theorem: MProd.mk.arg_fstsnd.revDerivUpdate_rule
Proof state before:
case h.h.h
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : W
dy : MProd X Y
dx : W
⊢ dx + ((revDeriv K (fun w => f w) x).2 dy.fst + (revDeriv K (fun w => g w) x).2 dy.snd) =
    dx + (revDeriv K g x).2 dy.snd + (revDeriv K f x).2 dy.fst
Tactic:
simp[add_assoc]
Proof state after:
case h.h.h
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : W
dy : MProd X Y
dx : W
⊢ (revDeriv K (fun w => f w) x).2 dy.fst + (revDeriv K (fun w => g w) x).2 dy.snd =
    (revDeriv K g x).2 dy.snd + (revDeriv K f x).2 dy.fst
Theorem: MProd.mk.arg_fstsnd.revDerivUpdate_rule
Proof state before:
case h.h.h
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : W
dy : MProd X Y
dx : W
⊢ (revDeriv K (fun w => f w) x).2 dy.fst + (revDeriv K (fun w => g w) x).2 dy.snd =
    (revDeriv K g x).2 dy.snd + (revDeriv K f x).2 dy.fst
Tactic:
rw[add_comm]
Proof state after:
no goals
Theorem: MProd.fst.arg_self.HasAdjDiff_rule
Proof state before:
K : Type u_2
inst✝³ : RCLike K
X : Type u_1
inst✝² : SemiInnerProductSpace K X
Y : Type u_1
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_3
inst✝ : SemiInnerProductSpace K W
f : W → MProd X Y
hf : HasAdjDiff K f
⊢ HasAdjDiff K fun w => (f w).fst
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: MProd.fst.arg_self.revDeriv_rule
Proof state before:
K : Type u_2
inst✝³ : RCLike K
X : Type u_1
inst✝² : SemiInnerProductSpace K X
Y : Type u_1
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_3
inst✝ : SemiInnerProductSpace K W
f : W → MProd X Y
hf : HasAdjDiff K f
⊢ (revDeriv K fun w => (f w).fst) = fun w =>
    let xydxy := revDeriv K f w;
    (xydxy.1.fst, fun dw => xydxy.2 { fst := dw, snd := 0 })
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: MProd.fst.arg_self.revDerivUpdate_rule
Proof state before:
K : Type u_2
inst✝³ : RCLike K
X : Type u_1
inst✝² : SemiInnerProductSpace K X
Y : Type u_1
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_3
inst✝ : SemiInnerProductSpace K W
f : W → MProd X Y
hf : HasAdjDiff K f
⊢ (revDerivUpdate K fun w => (f w).fst) = fun w =>
    let xydxy := revDerivUpdate K f w;
    (xydxy.1.fst, fun dx' dw => xydxy.2 { fst := dx', snd := 0 } dw)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: MProd.snd.arg_self.HasAdjDiff_rule
Proof state before:
K : Type u_2
inst✝³ : RCLike K
X : Type u_1
inst✝² : SemiInnerProductSpace K X
Y : Type u_1
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_3
inst✝ : SemiInnerProductSpace K W
f : W → MProd X Y
hf : HasAdjDiff K f
⊢ HasAdjDiff K fun w => (f w).snd
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: MProd.snd.arg_self.revDeriv_rule
Proof state before:
K : Type u_2
inst✝³ : RCLike K
X : Type u_1
inst✝² : SemiInnerProductSpace K X
Y : Type u_1
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_3
inst✝ : SemiInnerProductSpace K W
f : W → MProd X Y
hf : HasAdjDiff K f
⊢ (revDeriv K fun w => (f w).snd) = fun w =>
    let xydxy := revDeriv K f w;
    (xydxy.1.snd, fun dy' => xydxy.2 { fst := 0, snd := dy' })
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: MProd.snd.arg_self.revDerivUpdate_rule
Proof state before:
K : Type u_2
inst✝³ : RCLike K
X : Type u_1
inst✝² : SemiInnerProductSpace K X
Y : Type u_1
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_3
inst✝ : SemiInnerProductSpace K W
f : W → MProd X Y
hf : HasAdjDiff K f
⊢ (revDerivUpdate K fun w => (f w).snd) = fun w =>
    let xydxy := revDerivUpdate K f w;
    (xydxy.1.snd, fun dy' dw => xydxy.2 { fst := 0, snd := dy' } dw)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Rand.uniformI.pdf
Proof state before:
R : Type
inst✝¹ : RealScalar R
inst✝ : MeasureSpace R
⊢ Rand.pdf R (uniformI R) volume = fun x => if 0 < x ∧ x < 1 then 1 else 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.erase_out
Proof state before:
α : Sort u_1
a : α
⊢ Erased.out (erase a) = a
Tactic:
simp[erase]
Proof state after:
no goals
Theorem: SciLean.Rand.swap_bind
Proof state before:
X Y Z : Type
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace Y
f : X → Y → Z
x : Rand X
y : Rand Y
⊢ (do
      let x' ← x
      let y' ← y
      pure (f x' y')) =
    do
    let y' ← y
    let x' ← x
    pure (f x' y')
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Rand.pure_𝔼
Proof state before:
X : Type
Y : Type u_1
Z : Type ?u.67988
inst✝⁸ : MeasurableSpace X
inst✝⁷ : MeasurableSpace Y
R : Type ?u.68000
inst✝⁶ : RealScalar R
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : AddCommGroup Z
inst✝² : Module ℝ Z
U : Type ?u.69197
inst✝¹ : AddCommGroup U
inst✝ : Module ℝ U
x : X
φ : X → Y
⊢ (pure x).𝔼 φ = φ x
Tactic:
simp [𝔼]
Proof state after:
no goals
Theorem: SciLean.Rand.bind_E
Proof state before:
X Y : Type
Z : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : MeasurableSpace Y
R : Type ?u.70233
inst✝⁶ : RealScalar R
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : AddCommGroup Z
inst✝² : Module ℝ Z
U : Type ?u.71430
inst✝¹ : AddCommGroup U
inst✝ : Module ℝ U
r : Rand X
f : X → Rand Y
φ : Y → Z
⊢ (r >>= f).𝔼 φ = r.𝔼 fun x' => (f x').𝔼 φ
Tactic:
simp[𝔼]
Proof state after:
X Y : Type
Z : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : MeasurableSpace Y
R : Type ?u.70233
inst✝⁶ : RealScalar R
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : AddCommGroup Z
inst✝² : Module ℝ Z
U : Type ?u.71430
inst✝¹ : AddCommGroup U
inst✝ : Module ℝ U
r : Rand X
f : X → Rand Y
φ : Y → Z
⊢ ∫' x, φ x ∂(r >>= f).ℙ = ∫' x, ∫' x, φ x ∂(f x).ℙ ∂r.ℙ
Theorem: SciLean.Rand.bind_E
Proof state before:
X Y : Type
Z : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : MeasurableSpace Y
R : Type ?u.70233
inst✝⁶ : RealScalar R
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : AddCommGroup Z
inst✝² : Module ℝ Z
U : Type ?u.71430
inst✝¹ : AddCommGroup U
inst✝ : Module ℝ U
r : Rand X
f : X → Rand Y
φ : Y → Z
⊢ ∫' x, φ x ∂(r >>= f).ℙ = ∫' x, ∫' x, φ x ∂(f x).ℙ ∂r.ℙ
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Rand.E_zero
Proof state before:
X : Type
Y : Type ?u.73440
Z : Type ?u.73443
inst✝⁸ : MeasurableSpace X
inst✝⁷ : MeasurableSpace Y
R : Type ?u.73455
inst✝⁶ : RealScalar R
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : AddCommGroup Z
inst✝² : Module ℝ Z
U : Type u_1
inst✝¹ : AddCommGroup U
inst✝ : Module ℝ U
r : Rand X
⊢ (r.𝔼 fun x => 0) = 0
Tactic:
simp[𝔼]
Proof state after:
no goals
Theorem: SciLean.Rand.E_add
Proof state before:
X : Type
Y : Type ?u.76652
Z : Type ?u.76655
inst✝⁸ : MeasurableSpace X
inst✝⁷ : MeasurableSpace Y
R : Type ?u.76667
inst✝⁶ : RealScalar R
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : AddCommGroup Z
inst✝² : Module ℝ Z
U : Type u_1
inst✝¹ : AddCommGroup U
inst✝ : Module ℝ U
r : Rand X
φ ψ : X → U
hφ : CIntegrable φ r.ℙ
hψ : CIntegrable ψ r.ℙ
⊢ (r.𝔼 fun x => φ x + ψ x) = r.𝔼 φ + r.𝔼 ψ
Tactic:
simp[𝔼]
Proof state after:
X : Type
Y : Type ?u.76652
Z : Type ?u.76655
inst✝⁸ : MeasurableSpace X
inst✝⁷ : MeasurableSpace Y
R : Type ?u.76667
inst✝⁶ : RealScalar R
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : AddCommGroup Z
inst✝² : Module ℝ Z
U : Type u_1
inst✝¹ : AddCommGroup U
inst✝ : Module ℝ U
r : Rand X
φ ψ : X → U
hφ : CIntegrable φ r.ℙ
hψ : CIntegrable ψ r.ℙ
⊢ ∫' x, φ x + ψ x ∂r.ℙ = ∫' x, φ x ∂r.ℙ + ∫' x, ψ x ∂r.ℙ
Theorem: SciLean.Rand.E_add
Proof state before:
X : Type
Y : Type ?u.76652
Z : Type ?u.76655
inst✝⁸ : MeasurableSpace X
inst✝⁷ : MeasurableSpace Y
R : Type ?u.76667
inst✝⁶ : RealScalar R
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : AddCommGroup Z
inst✝² : Module ℝ Z
U : Type u_1
inst✝¹ : AddCommGroup U
inst✝ : Module ℝ U
r : Rand X
φ ψ : X → U
hφ : CIntegrable φ r.ℙ
hψ : CIntegrable ψ r.ℙ
⊢ ∫' x, φ x + ψ x ∂r.ℙ = ∫' x, φ x ∂r.ℙ + ∫' x, ψ x ∂r.ℙ
Tactic:
rw[cintegral_add] <;> assumption
Proof state after:
no goals
Theorem: SciLean.Rand.E_smul
Proof state before:
X : Type
Y : Type u_1
Z : Type ?u.82732
inst✝⁸ : MeasurableSpace X
inst✝⁷ : MeasurableSpace Y
R : Type ?u.82744
inst✝⁶ : RealScalar R
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : AddCommGroup Z
inst✝² : Module ℝ Z
U : Type ?u.83941
inst✝¹ : AddCommGroup U
inst✝ : Module ℝ U
r : Rand X
φ : X → ℝ
y : Y
⊢ (r.𝔼 fun x' => φ x' • y) = r.𝔼 φ • y
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Rand.reparameterize
Proof state before:
X Y : Type
Z : Type u_1
inst✝⁹ : MeasurableSpace X
inst✝⁸ : MeasurableSpace Y
R : Type ?u.86975
inst✝⁷ : RealScalar R
inst✝⁶ : AddCommGroup Y
inst✝⁵ : Module ℝ Y
inst✝⁴ : AddCommGroup Z
inst✝³ : Module ℝ Z
U : Type ?u.88172
inst✝² : AddCommGroup U
inst✝¹ : Module ℝ U
inst✝ : Nonempty X
f : X → Y
hf : Function.Injective f
r : Rand X
φ : X → Z
⊢ r.𝔼 φ =
    let invf := Function.invFun f;
    (r.map f).𝔼 fun y => φ (invf y)
Tactic:
simp [𝔼,Function.invFun_comp' hf]
Proof state after:
no goals
Theorem: SciLean.Rand.expectedValue_as_mean
Proof state before:
X Y : Type
Z : Type ?u.95201
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : MeasurableSpace Y
R : Type ?u.95213
inst✝⁸ : RealScalar R
inst✝⁷ : AddCommGroup Y
inst✝⁶ : Module ℝ Y
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
U : Type ?u.96410
inst✝³ : AddCommGroup U
inst✝² : Module ℝ U
inst✝¹ : AddCommGroup X
inst✝ : Module ℝ X
x : Rand X
φ : X → Y
⊢ x.𝔼 φ = mean (x.map φ)
Tactic:
simp [bind,mean,pure,𝔼]
Proof state after:
no goals
Theorem: SciLean.Rand.pure_mean
Proof state before:
X : Type
Y : Type ?u.98701
Z : Type ?u.98704
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : MeasurableSpace Y
R : Type ?u.98716
inst✝⁸ : RealScalar R
inst✝⁷ : AddCommGroup Y
inst✝⁶ : Module ℝ Y
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
U : Type ?u.99913
inst✝³ : AddCommGroup U
inst✝² : Module ℝ U
inst✝¹ : AddCommGroup X
inst✝ : Module ℝ X
x : X
⊢ mean (pure x) = x
Tactic:
simp[mean]
Proof state after:
no goals
Theorem: SciLean.Rand.bind_mean
Proof state before:
X Y : Type
Z : Type ?u.101457
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : MeasurableSpace Y
R : Type ?u.101469
inst✝⁸ : RealScalar R
inst✝⁷ : AddCommGroup Y
inst✝⁶ : Module ℝ Y
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
U : Type ?u.102666
inst✝³ : AddCommGroup U
inst✝² : Module ℝ U
inst✝¹ : AddCommGroup X
inst✝ : Module ℝ X
x : Rand X
f : X → Rand Y
⊢ mean (x >>= f) = x.𝔼 fun x' => mean (f x')
Tactic:
simp[mean,rand_push_E]
Proof state after:
no goals
Theorem: SciLean.Rand.mean_add
Proof state before:
X : Type
Y : Type ?u.105470
Z : Type ?u.105473
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : MeasurableSpace Y
R : Type ?u.105485
inst✝⁸ : RealScalar R
inst✝⁷ : AddCommGroup Y
inst✝⁶ : Module ℝ Y
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
U : Type ?u.106682
inst✝³ : AddCommGroup U
inst✝² : Module ℝ U
inst✝¹ : AddCommGroup X
inst✝ : Module ℝ X
x : Rand X
x' : X
⊢ mean x + x' = mean (x + x')
Tactic:
simp[HAdd.hAdd,mean,𝔼,pure,bind]
Proof state after:
X : Type
Y : Type ?u.105470
Z : Type ?u.105473
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : MeasurableSpace Y
R : Type ?u.105485
inst✝⁸ : RealScalar R
inst✝⁷ : AddCommGroup Y
inst✝⁶ : Module ℝ Y
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
U : Type ?u.106682
inst✝³ : AddCommGroup U
inst✝² : Module ℝ U
inst✝¹ : AddCommGroup X
inst✝ : Module ℝ X
x : Rand X
x' : X
⊢ Add.add (∫' x, x ∂x.ℙ) x' =
    ∫' x,
      x ∂{ spec := erase fun φ => Erased.out x.spec fun x => φ (Add.add x x'),
          rand := StateT.bind x.rand fun x => StateT.pure (Add.add x x') }.ℙ
Theorem: SciLean.Rand.mean_add
Proof state before:
X : Type
Y : Type ?u.105470
Z : Type ?u.105473
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : MeasurableSpace Y
R : Type ?u.105485
inst✝⁸ : RealScalar R
inst✝⁷ : AddCommGroup Y
inst✝⁶ : Module ℝ Y
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
U : Type ?u.106682
inst✝³ : AddCommGroup U
inst✝² : Module ℝ U
inst✝¹ : AddCommGroup X
inst✝ : Module ℝ X
x : Rand X
x' : X
⊢ Add.add (∫' x, x ∂x.ℙ) x' =
    ∫' x,
      x ∂{ spec := erase fun φ => Erased.out x.spec fun x => φ (Add.add x x'),
          rand := StateT.bind x.rand fun x => StateT.pure (Add.add x x') }.ℙ
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Rand.mean_add'
Proof state before:
X : Type
Y : Type ?u.114836
Z : Type ?u.114839
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : MeasurableSpace Y
R : Type ?u.114851
inst✝⁸ : RealScalar R
inst✝⁷ : AddCommGroup Y
inst✝⁶ : Module ℝ Y
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
U : Type ?u.116048
inst✝³ : AddCommGroup U
inst✝² : Module ℝ U
inst✝¹ : AddCommGroup X
inst✝ : Module ℝ X
x : Rand X
x' : X
⊢ x' + mean x = mean (x' + x)
Tactic:
simp[HAdd.hAdd,mean,𝔼,pure,bind]
Proof state after:
X : Type
Y : Type ?u.114836
Z : Type ?u.114839
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : MeasurableSpace Y
R : Type ?u.114851
inst✝⁸ : RealScalar R
inst✝⁷ : AddCommGroup Y
inst✝⁶ : Module ℝ Y
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
U : Type ?u.116048
inst✝³ : AddCommGroup U
inst✝² : Module ℝ U
inst✝¹ : AddCommGroup X
inst✝ : Module ℝ X
x : Rand X
x' : X
⊢ Add.add x' (∫' x, x ∂x.ℙ) =
    ∫' x,
      x ∂{ spec := erase fun φ => Erased.out x.spec fun x => φ (Add.add x' x),
          rand := StateT.bind x.rand fun x => StateT.pure (Add.add x' x) }.ℙ
Theorem: SciLean.Rand.mean_add'
Proof state before:
X : Type
Y : Type ?u.114836
Z : Type ?u.114839
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : MeasurableSpace Y
R : Type ?u.114851
inst✝⁸ : RealScalar R
inst✝⁷ : AddCommGroup Y
inst✝⁶ : Module ℝ Y
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
U : Type ?u.116048
inst✝³ : AddCommGroup U
inst✝² : Module ℝ U
inst✝¹ : AddCommGroup X
inst✝ : Module ℝ X
x : Rand X
x' : X
⊢ Add.add x' (∫' x, x ∂x.ℙ) =
    ∫' x,
      x ∂{ spec := erase fun φ => Erased.out x.spec fun x => φ (Add.add x' x),
          rand := StateT.bind x.rand fun x => StateT.pure (Add.add x' x) }.ℙ
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Rand.bind_pdf
Proof state before:
X Y : Type
Z : Type ?u.124691
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
R : Type u_1
inst✝² : RealScalar R
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace Y
ν : Measure Y
x : Rand X
f : X → Rand Y
⊢ pdf R (x >>= f) ν = fun y => ∫ (x' : X), pdf R (f x') ν y ∂x.ℙ
Tactic:
funext y
Proof state after:
case h
X Y : Type
Z : Type ?u.124691
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
R : Type u_1
inst✝² : RealScalar R
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace Y
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ pdf R (x >>= f) ν y = ∫ (x' : X), pdf R (f x') ν y ∂x.ℙ
Theorem: SciLean.Rand.bind_pdf
Proof state before:
case h
X Y : Type
Z : Type ?u.124691
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
R : Type u_1
inst✝² : RealScalar R
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace Y
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ pdf R (x >>= f) ν y = ∫ (x' : X), pdf R (f x') ν y ∂x.ℙ
Tactic:
simp[Rand.pdf,Bind.bind,Pure.pure]
Proof state after:
case h
X Y : Type
Z : Type ?u.124691
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
R : Type u_1
inst✝² : RealScalar R
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace Y
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ Scalar.ofReal R
      ({ spec := erase fun φ => Erased.out x.spec fun x => Erased.out (f x).spec φ,
                rand := StateT.bind x.rand fun x => (f x).rand }.ℙ.rnDeriv
          ν y).toReal =
    ∫ (x' : X), Scalar.ofReal R ((f x').ℙ.rnDeriv ν y).toReal ∂x.ℙ
Theorem: SciLean.Rand.bind_pdf
Proof state before:
case h
X Y : Type
Z : Type ?u.124691
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
R : Type u_1
inst✝² : RealScalar R
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace Y
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ Scalar.ofReal R
      ({ spec := erase fun φ => Erased.out x.spec fun x => Erased.out (f x).spec φ,
                rand := StateT.bind x.rand fun x => (f x).rand }.ℙ.rnDeriv
          ν y).toReal =
    ∫ (x' : X), Scalar.ofReal R ((f x').ℙ.rnDeriv ν y).toReal ∂x.ℙ
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Rand.ite_pdf
Proof state before:
X : Type
Y : Type ?u.127136
Z : Type ?u.127139
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
R : Type u_1
inst✝³ : RealScalar R
inst✝² : MeasurableSpace X
inst✝¹ : MeasurableSpace Y
c : Prop
inst✝ : Decidable c
t e : Rand X
μ : Measure X
⊢ pdf R (if c then t else e) μ = if c then pdf R t μ else pdf R e μ
Tactic:
if h : c then
  simp [h]
else
  simp [h]
Proof state after:
no goals
Theorem: SciLean.Rand.ite_pdf
Proof state before:
X : Type
Y : Type ?u.127136
Z : Type ?u.127139
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
R : Type u_1
inst✝³ : RealScalar R
inst✝² : MeasurableSpace X
inst✝¹ : MeasurableSpace Y
c : Prop
inst✝ : Decidable c
t e : Rand X
μ : Measure X
h : c
⊢ pdf R (if c then t else e) μ = if c then pdf R t μ else pdf R e μ
Tactic:
simp [h]
Proof state after:
no goals
Theorem: SciLean.Rand.ite_pdf
Proof state before:
X : Type
Y : Type ?u.127136
Z : Type ?u.127139
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
R : Type u_1
inst✝³ : RealScalar R
inst✝² : MeasurableSpace X
inst✝¹ : MeasurableSpace Y
c : Prop
inst✝ : Decidable c
t e : Rand X
μ : Measure X
h : ¬c
⊢ pdf R (if c then t else e) μ = if c then pdf R t μ else pdf R e μ
Tactic:
simp [h]
Proof state after:
no goals
Theorem: SciLean.Alternatives.pick_fst
Proof state before:
α : Sort u_1
a b : α
ap : Alternatives a b
⊢ choose a b ap = a
Tactic:
unfold Alternatives.choose
Proof state after:
α : Sort u_1
a b : α
ap : Alternatives a b
⊢ a = a
Theorem: SciLean.Alternatives.pick_fst
Proof state before:
α : Sort u_1
a b : α
ap : Alternatives a b
⊢ a = a
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.Alternatives.pick_snd
Proof state before:
α : Sort u_1
a b : α
ap : Alternatives a b
⊢ choose a b ap = b
Tactic:
unfold Alternatives.choose
Proof state after:
α : Sort u_1
a b : α
ap : Alternatives a b
⊢ a = b
Theorem: SciLean.Alternatives.pick_snd
Proof state before:
α : Sort u_1
a b : α
ap : Alternatives a b
⊢ a = b
Tactic:
rw [ap.eq]
Proof state after:
no goals