internlm/Lean-Github huggingface dataset:
Theorem: SciLean.Scalar.cos.arg_x.HasAdjDiff_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.11071
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasAdjDiffAt C (fun u => cos (x✝ u)) x
Tactic:
constructor
Proof state after:
case left
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.11071
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ CDifferentiableAt C (fun u => cos (x✝ u)) x

case right
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.11071
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C (cderiv C (fun u => cos (x✝ u)) x)
Theorem: SciLean.Scalar.cos.arg_x.HasAdjDiff_rule
Proof state before:
case left
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.11071
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ CDifferentiableAt C (fun u => cos (x✝ u)) x

case right
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.11071
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C (cderiv C (fun u => cos (x✝ u)) x)
Tactic:
fun_prop
Proof state after:
case right
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.11071
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C (cderiv C (fun u => cos (x✝ u)) x)
Theorem: SciLean.Scalar.cos.arg_x.HasAdjDiff_rule
Proof state before:
case right
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.11071
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C (cderiv C (fun u => cos (x✝ u)) x)
Tactic:
fun_trans [fwdDeriv]
Proof state after:
case right
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.11071
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C fun dw => -(cderiv C (fun w => x✝ w) x dw * sin (x✝ x))
Theorem: SciLean.Scalar.cos.arg_x.HasAdjDiff_rule
Proof state before:
case right
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.11071
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C fun dw => -(cderiv C (fun w => x✝ w) x dw * sin (x✝ x))
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.Scalar.cos.arg_x.revDeriv_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.13258
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x : U → C
hx : HasAdjDiff C x
⊢ (revDeriv C fun u => cos (x u)) = fun u =>
    let xdx := revDeriv C x u;
    (cos xdx.1, fun dy => xdx.2 (-(starRingEnd C) (sin xdx.1) * dy))
Tactic:
unfold revDeriv
Proof state after:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.13258
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x : U → C
hx : HasAdjDiff C x
⊢ (fun x_1 => ((fun u => cos (x u)) x_1, semiAdjoint C (cderiv C (fun u => cos (x u)) x_1))) = fun u =>
    let xdx := (x u, semiAdjoint C (cderiv C x u));
    (cos xdx.1, fun dy => xdx.2 (-(starRingEnd C) (sin xdx.1) * dy))
Theorem: SciLean.Scalar.cos.arg_x.revDeriv_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.13258
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x : U → C
hx : HasAdjDiff C x
⊢ (fun x_1 => ((fun u => cos (x u)) x_1, semiAdjoint C (cderiv C (fun u => cos (x u)) x_1))) = fun u =>
    let xdx := (x u, semiAdjoint C (cderiv C x u));
    (cos xdx.1, fun dy => xdx.2 (-(starRingEnd C) (sin xdx.1) * dy))
Tactic:
fun_trans only [fwdDeriv, smul_push, neg_push, ftrans_simp]
Proof state after:
no goals
Theorem: SciLean.Scalar.tanh.arg_x.fwdDeriv_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.17106
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fwdDeriv C fun w => tanh (x w)) = fun w dw =>
    let xdx := fwdDeriv C x w dw;
    let t := tanh xdx.1;
    let dt := 1 - t ^ 2;
    (t, xdx.2 * dt)
Tactic:
unfold fwdDeriv
Proof state after:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.17106
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fun x_1 dx => ((fun w => tanh (x w)) x_1, cderiv C (fun w => tanh (x w)) x_1 dx)) = fun w dw =>
    let xdx := (x w, cderiv C x w dw);
    let t := tanh xdx.1;
    let dt := 1 - t ^ 2;
    (t, xdx.2 * dt)
Theorem: SciLean.Scalar.tanh.arg_x.fwdDeriv_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.17106
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fun x_1 dx => ((fun w => tanh (x w)) x_1, cderiv C (fun w => tanh (x w)) x_1 dx)) = fun w dw =>
    let xdx := (x w, cderiv C x w dw);
    let t := tanh xdx.1;
    let dt := 1 - t ^ 2;
    (t, xdx.2 * dt)
Tactic:
fun_trans
Proof state after:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.17106
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fun x_1 dx =>
      (tanh (x x_1), (fwdDeriv C (fun w => x w) x_1 dx).2 * (1 - tanh (fwdDeriv C (fun w => x w) x_1 dx).1 ^ 2))) =
    fun w dw => (tanh (x w), cderiv C x w dw * (1 - tanh (x w) ^ 2))
Theorem: SciLean.Scalar.tanh.arg_x.fwdDeriv_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.17106
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fun x_1 dx =>
      (tanh (x x_1), (fwdDeriv C (fun w => x w) x_1 dx).2 * (1 - tanh (fwdDeriv C (fun w => x w) x_1 dx).1 ^ 2))) =
    fun w dw => (tanh (x w), cderiv C x w dw * (1 - tanh (x w) ^ 2))
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.Scalar.tanh.arg_x.HasAdjDiff_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.21883
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x : U → C
hx : HasAdjDiff C x
⊢ HasAdjDiff C fun u => tanh (x u)
Tactic:
intro x
Proof state after:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.21883
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasAdjDiffAt C (fun u => tanh (x✝ u)) x
Theorem: SciLean.Scalar.tanh.arg_x.HasAdjDiff_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.21883
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasAdjDiffAt C (fun u => tanh (x✝ u)) x
Tactic:
constructor
Proof state after:
case left
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.21883
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ CDifferentiableAt C (fun u => tanh (x✝ u)) x

case right
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.21883
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C (cderiv C (fun u => tanh (x✝ u)) x)
Theorem: SciLean.Scalar.tanh.arg_x.HasAdjDiff_rule
Proof state before:
case left
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.21883
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ CDifferentiableAt C (fun u => tanh (x✝ u)) x

case right
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.21883
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C (cderiv C (fun u => tanh (x✝ u)) x)
Tactic:
fun_prop
Proof state after:
case right
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.21883
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C (cderiv C (fun u => tanh (x✝ u)) x)
Theorem: SciLean.Scalar.tanh.arg_x.HasAdjDiff_rule
Proof state before:
case right
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.21883
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C (cderiv C (fun u => tanh (x✝ u)) x)
Tactic:
fun_trans [fwdDeriv]
Proof state after:
case right
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.21883
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C fun dw => cderiv C (fun w => x✝ w) x dw * (1 - tanh (x✝ x) ^ 2)
Theorem: SciLean.Scalar.tanh.arg_x.HasAdjDiff_rule
Proof state before:
case right
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.21883
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C fun dw => cderiv C (fun w => x✝ w) x dw * (1 - tanh (x✝ x) ^ 2)
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.Scalar.tanh.arg_x.revDeriv_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.24680
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x : U → C
hx : HasAdjDiff C x
⊢ (revDeriv C fun u => tanh (x u)) = fun u =>
    let xdx := revDeriv C x u;
    (tanh xdx.1, fun dy => xdx.2 ((starRingEnd C) (1 - tanh xdx.1 ^ 2) * dy))
Tactic:
unfold revDeriv
Proof state after:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.24680
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x : U → C
hx : HasAdjDiff C x
⊢ (fun x_1 => ((fun u => tanh (x u)) x_1, semiAdjoint C (cderiv C (fun u => tanh (x u)) x_1))) = fun u =>
    let xdx := (x u, semiAdjoint C (cderiv C x u));
    (tanh xdx.1, fun dy => xdx.2 ((starRingEnd C) (1 - tanh xdx.1 ^ 2) * dy))
Theorem: SciLean.Scalar.tanh.arg_x.revDeriv_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.24680
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x : U → C
hx : HasAdjDiff C x
⊢ (fun x_1 => ((fun u => tanh (x u)) x_1, semiAdjoint C (cderiv C (fun u => tanh (x u)) x_1))) = fun u =>
    let xdx := (x u, semiAdjoint C (cderiv C x u));
    (tanh xdx.1, fun dy => xdx.2 ((starRingEnd C) (1 - tanh xdx.1 ^ 2) * dy))
Tactic:
fun_trans only [fwdDeriv, smul_push, ftrans_simp]
Proof state after:
no goals
Theorem: SciLean.Rand.bind_pull_mean
Proof state before:
R : Type ?u.1821
inst✝⁸ : RealScalar R
X : Type
inst✝⁷ : MeasurableSpace X
inst✝⁶ : AddCommGroup X
inst✝⁵ : Module ℝ X
Y : Type
inst✝⁴ : AddCommGroup Y
inst✝³ : Module ℝ Y
inst✝² : MeasurableSpace Y
Z : Type ?u.3033
inst✝¹ : AddCommGroup Z
inst✝ : Module ℝ Z
x : Rand X
f : X → Rand Y
⊢ (mean do
      let x' ← x
      pure (mean (f x'))) =
    mean (x >>= f)
Tactic:
simp[rand_push_E]
Proof state after:
no goals
Theorem: SciLean.Rand.ite_push_E
Proof state before:
R : Type ?u.5678
inst✝⁹ : RealScalar R
X : Type
inst✝⁸ : MeasurableSpace X
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module ℝ X
Y : Type u_1
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : MeasurableSpace Y
Z : Type ?u.6890
inst✝² : AddCommGroup Z
inst✝¹ : Module ℝ Z
c : Prop
inst✝ : Decidable c
t e : Rand X
φ : X → Y
⊢ (if c then t else e).𝔼 φ = if c then t.𝔼 φ else e.𝔼 φ
Tactic:
if h : c then simp[h] else simp[h]
Proof state after:
no goals
Theorem: SciLean.Rand.ite_push_E
Proof state before:
R : Type ?u.5678
inst✝⁹ : RealScalar R
X : Type
inst✝⁸ : MeasurableSpace X
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module ℝ X
Y : Type u_1
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : MeasurableSpace Y
Z : Type ?u.6890
inst✝² : AddCommGroup Z
inst✝¹ : Module ℝ Z
c : Prop
inst✝ : Decidable c
t e : Rand X
φ : X → Y
h : c
⊢ (if c then t else e).𝔼 φ = if c then t.𝔼 φ else e.𝔼 φ
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Rand.ite_push_E
Proof state before:
R : Type ?u.5678
inst✝⁹ : RealScalar R
X : Type
inst✝⁸ : MeasurableSpace X
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module ℝ X
Y : Type u_1
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : MeasurableSpace Y
Z : Type ?u.6890
inst✝² : AddCommGroup Z
inst✝¹ : Module ℝ Z
c : Prop
inst✝ : Decidable c
t e : Rand X
φ : X → Y
h : ¬c
⊢ (if c then t else e).𝔼 φ = if c then t.𝔼 φ else e.𝔼 φ
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Rand.ite_pull_E
Proof state before:
R : Type ?u.8434
inst✝⁹ : RealScalar R
X : Type
inst✝⁸ : MeasurableSpace X
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module ℝ X
Y : Type u_1
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : MeasurableSpace Y
Z : Type ?u.9646
inst✝² : AddCommGroup Z
inst✝¹ : Module ℝ Z
c : Prop
inst✝ : Decidable c
t e : Rand X
φ ψ : X → Y
⊢ (if c then t.𝔼 φ else e.𝔼 ψ) = (if c then t else e).𝔼 (if c then φ else ψ)
Tactic:
if h : c then simp[h] else simp[h]
Proof state after:
no goals
Theorem: SciLean.Rand.ite_pull_E
Proof state before:
R : Type ?u.8434
inst✝⁹ : RealScalar R
X : Type
inst✝⁸ : MeasurableSpace X
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module ℝ X
Y : Type u_1
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : MeasurableSpace Y
Z : Type ?u.9646
inst✝² : AddCommGroup Z
inst✝¹ : Module ℝ Z
c : Prop
inst✝ : Decidable c
t e : Rand X
φ ψ : X → Y
h : c
⊢ (if c then t.𝔼 φ else e.𝔼 ψ) = (if c then t else e).𝔼 (if c then φ else ψ)
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Rand.ite_pull_E
Proof state before:
R : Type ?u.8434
inst✝⁹ : RealScalar R
X : Type
inst✝⁸ : MeasurableSpace X
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module ℝ X
Y : Type u_1
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : MeasurableSpace Y
Z : Type ?u.9646
inst✝² : AddCommGroup Z
inst✝¹ : Module ℝ Z
c : Prop
inst✝ : Decidable c
t e : Rand X
φ ψ : X → Y
h : ¬c
⊢ (if c then t.𝔼 φ else e.𝔼 ψ) = (if c then t else e).𝔼 (if c then φ else ψ)
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Rand.ite_push_mean
Proof state before:
R : Type ?u.11167
inst✝⁹ : RealScalar R
X : Type
inst✝⁸ : MeasurableSpace X
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module ℝ X
Y : Type ?u.11775
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : MeasurableSpace Y
Z : Type ?u.12379
inst✝² : AddCommGroup Z
inst✝¹ : Module ℝ Z
c : Prop
inst✝ : Decidable c
t e : Rand X
⊢ mean (if c then t else e) = if c then mean t else mean e
Tactic:
if h : c then simp[h] else simp[h]
Proof state after:
no goals
Theorem: SciLean.Rand.ite_push_mean
Proof state before:
R : Type ?u.11167
inst✝⁹ : RealScalar R
X : Type
inst✝⁸ : MeasurableSpace X
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module ℝ X
Y : Type ?u.11775
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : MeasurableSpace Y
Z : Type ?u.12379
inst✝² : AddCommGroup Z
inst✝¹ : Module ℝ Z
c : Prop
inst✝ : Decidable c
t e : Rand X
h : c
⊢ mean (if c then t else e) = if c then mean t else mean e
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Rand.ite_push_mean
Proof state before:
R : Type ?u.11167
inst✝⁹ : RealScalar R
X : Type
inst✝⁸ : MeasurableSpace X
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module ℝ X
Y : Type ?u.11775
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : MeasurableSpace Y
Z : Type ?u.12379
inst✝² : AddCommGroup Z
inst✝¹ : Module ℝ Z
c : Prop
inst✝ : Decidable c
t e : Rand X
h : ¬c
⊢ mean (if c then t else e) = if c then mean t else mean e
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Rand.ite_pull_mean
Proof state before:
R : Type ?u.13194
inst✝⁹ : RealScalar R
X : Type
inst✝⁸ : MeasurableSpace X
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module ℝ X
Y : Type ?u.13802
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : MeasurableSpace Y
Z : Type ?u.14406
inst✝² : AddCommGroup Z
inst✝¹ : Module ℝ Z
c : Prop
inst✝ : Decidable c
t e : Rand X
⊢ (if c then mean t else mean e) = mean (if c then t else e)
Tactic:
if h : c then simp[h] else simp[h]
Proof state after:
no goals
Theorem: SciLean.Rand.ite_pull_mean
Proof state before:
R : Type ?u.13194
inst✝⁹ : RealScalar R
X : Type
inst✝⁸ : MeasurableSpace X
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module ℝ X
Y : Type ?u.13802
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : MeasurableSpace Y
Z : Type ?u.14406
inst✝² : AddCommGroup Z
inst✝¹ : Module ℝ Z
c : Prop
inst✝ : Decidable c
t e : Rand X
h : c
⊢ (if c then mean t else mean e) = mean (if c then t else e)
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Rand.ite_pull_mean
Proof state before:
R : Type ?u.13194
inst✝⁹ : RealScalar R
X : Type
inst✝⁸ : MeasurableSpace X
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module ℝ X
Y : Type ?u.13802
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : MeasurableSpace Y
Z : Type ?u.14406
inst✝² : AddCommGroup Z
inst✝¹ : Module ℝ Z
c : Prop
inst✝ : Decidable c
t e : Rand X
h : ¬c
⊢ (if c then mean t else mean e) = mean (if c then t else e)
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Rand.ite_pull_mean_t
Proof state before:
R : Type ?u.15219
inst✝⁹ : RealScalar R
X : Type
inst✝⁸ : MeasurableSpace X
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module ℝ X
Y : Type ?u.15827
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : MeasurableSpace Y
Z : Type ?u.16431
inst✝² : AddCommGroup Z
inst✝¹ : Module ℝ Z
c : Prop
inst✝ : Decidable c
t : Rand X
e : X
⊢ (if c then mean t else e) = mean (if c then t else pure e)
Tactic:
if h : c then simp[h] else simp[h]
Proof state after:
no goals
Theorem: SciLean.Rand.ite_pull_mean_t
Proof state before:
R : Type ?u.15219
inst✝⁹ : RealScalar R
X : Type
inst✝⁸ : MeasurableSpace X
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module ℝ X
Y : Type ?u.15827
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : MeasurableSpace Y
Z : Type ?u.16431
inst✝² : AddCommGroup Z
inst✝¹ : Module ℝ Z
c : Prop
inst✝ : Decidable c
t : Rand X
e : X
h : c
⊢ (if c then mean t else e) = mean (if c then t else pure e)
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Rand.ite_pull_mean_t
Proof state before:
R : Type ?u.15219
inst✝⁹ : RealScalar R
X : Type
inst✝⁸ : MeasurableSpace X
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module ℝ X
Y : Type ?u.15827
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : MeasurableSpace Y
Z : Type ?u.16431
inst✝² : AddCommGroup Z
inst✝¹ : Module ℝ Z
c : Prop
inst✝ : Decidable c
t : Rand X
e : X
h : ¬c
⊢ (if c then mean t else e) = mean (if c then t else pure e)
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Rand.ite_pull_mean_f
Proof state before:
R : Type ?u.17418
inst✝⁹ : RealScalar R
X : Type
inst✝⁸ : MeasurableSpace X
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module ℝ X
Y : Type ?u.18026
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : MeasurableSpace Y
Z : Type ?u.18630
inst✝² : AddCommGroup Z
inst✝¹ : Module ℝ Z
c : Prop
inst✝ : Decidable c
t : X
e : Rand X
⊢ (if c then t else mean e) = mean (if c then pure t else e)
Tactic:
if h : c then simp[h] else simp[h]
Proof state after:
no goals
Theorem: SciLean.Rand.ite_pull_mean_f
Proof state before:
R : Type ?u.17418
inst✝⁹ : RealScalar R
X : Type
inst✝⁸ : MeasurableSpace X
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module ℝ X
Y : Type ?u.18026
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : MeasurableSpace Y
Z : Type ?u.18630
inst✝² : AddCommGroup Z
inst✝¹ : Module ℝ Z
c : Prop
inst✝ : Decidable c
t : X
e : Rand X
h : c
⊢ (if c then t else mean e) = mean (if c then pure t else e)
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Rand.ite_pull_mean_f
Proof state before:
R : Type ?u.17418
inst✝⁹ : RealScalar R
X : Type
inst✝⁸ : MeasurableSpace X
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module ℝ X
Y : Type ?u.18026
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : MeasurableSpace Y
Z : Type ?u.18630
inst✝² : AddCommGroup Z
inst✝¹ : Module ℝ Z
c : Prop
inst✝ : Decidable c
t : X
e : Rand X
h : ¬c
⊢ (if c then t else mean e) = mean (if c then pure t else e)
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Rand.pull_E_affine
Proof state before:
R : Type ?u.25032
inst✝⁸ : RealScalar R
X : Type
inst✝⁷ : MeasurableSpace X
inst✝⁶ : AddCommGroup X
inst✝⁵ : Module ℝ X
Y : Type u_1
inst✝⁴ : AddCommGroup Y
inst✝³ : Module ℝ Y
inst✝² : MeasurableSpace Y
Z : Type u_2
inst✝¹ : AddCommGroup Z
inst✝ : Module ℝ Z
r : Rand X
φ : X → Y
f : Y → Z
hf : autoParam (IsAffineMap ℝ f) _auto✝
⊢ f (r.𝔼 φ) = r.𝔼 fun x => f (φ x)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Rand.push_E_affine
Proof state before:
R : Type ?u.27379
inst✝⁸ : RealScalar R
X : Type
inst✝⁷ : MeasurableSpace X
inst✝⁶ : AddCommGroup X
inst✝⁵ : Module ℝ X
Y : Type u_1
inst✝⁴ : AddCommGroup Y
inst✝³ : Module ℝ Y
inst✝² : MeasurableSpace Y
Z : Type u_2
inst✝¹ : AddCommGroup Z
inst✝ : Module ℝ Z
r : Rand X
φ : X → Y
f : Y → Z
hf : autoParam (IsAffineMap ℝ f) _auto✝
⊢ (r.𝔼 fun x => f (φ x)) = f (r.𝔼 φ)
Tactic:
rw[pull_E_affine (hf:=hf)]
Proof state after:
no goals
Theorem: SciLean.Rand.pull_E_nat_recOn
Proof state before:
R : Type ?u.59471
inst✝¹³ : RealScalar R
X : Type ?u.59474
inst✝¹² : MeasurableSpace X
inst✝¹¹ : AddCommGroup X
inst✝¹⁰ : Module ℝ X
Y : Type ?u.60079
inst✝⁹ : AddCommGroup Y
inst✝⁸ : Module ℝ Y
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.60683
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module ℝ Z
C : ℕ → Type
inst✝⁴ : (n : ℕ) → AddCommGroup (C n)
inst✝³ : (n : ℕ) → Module ℝ (C n)
inst✝² : (n : ℕ) → MeasurableSpace (C n)
D : ℕ → Type
inst✝¹ inst✝ : (n : ℕ) → MeasurableSpace (D n)
n : ℕ
x₀ : C 0
r : (n : ℕ) → Rand (D n)
f : (n : ℕ) → C n → D n → C (n + 1)
hf : ∀ (n : ℕ) (d : D n), IsAffineMap ℝ fun x => f n x d
⊢ (Nat.recOn n x₀ fun n x => (r n).𝔼 (f n x)) =
    mean
      (Nat.recOn n (pure x₀) fun n x => do
        let x' ← x
        let y' ← r n
        pure (f n x' y'))
Tactic:
induction n
Proof state after:
case zero
R : Type ?u.59471
inst✝¹³ : RealScalar R
X : Type ?u.59474
inst✝¹² : MeasurableSpace X
inst✝¹¹ : AddCommGroup X
inst✝¹⁰ : Module ℝ X
Y : Type ?u.60079
inst✝⁹ : AddCommGroup Y
inst✝⁸ : Module ℝ Y
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.60683
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module ℝ Z
C : ℕ → Type
inst✝⁴ : (n : ℕ) → AddCommGroup (C n)
inst✝³ : (n : ℕ) → Module ℝ (C n)
inst✝² : (n : ℕ) → MeasurableSpace (C n)
D : ℕ → Type
inst✝¹ inst✝ : (n : ℕ) → MeasurableSpace (D n)
x₀ : C 0
r : (n : ℕ) → Rand (D n)
f : (n : ℕ) → C n → D n → C (n + 1)
hf : ∀ (n : ℕ) (d : D n), IsAffineMap ℝ fun x => f n x d
⊢ (Nat.recOn Nat.zero x₀ fun n x => (r n).𝔼 (f n x)) =
    mean
      (Nat.recOn Nat.zero (pure x₀) fun n x => do
        let x' ← x
        let y' ← r n
        pure (f n x' y'))

case succ
R : Type ?u.59471
inst✝¹³ : RealScalar R
X : Type ?u.59474
inst✝¹² : MeasurableSpace X
inst✝¹¹ : AddCommGroup X
inst✝¹⁰ : Module ℝ X
Y : Type ?u.60079
inst✝⁹ : AddCommGroup Y
inst✝⁸ : Module ℝ Y
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.60683
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module ℝ Z
C : ℕ → Type
inst✝⁴ : (n : ℕ) → AddCommGroup (C n)
inst✝³ : (n : ℕ) → Module ℝ (C n)
inst✝² : (n : ℕ) → MeasurableSpace (C n)
D : ℕ → Type
inst✝¹ inst✝ : (n : ℕ) → MeasurableSpace (D n)
x₀ : C 0
r : (n : ℕ) → Rand (D n)
f : (n : ℕ) → C n → D n → C (n + 1)
hf : ∀ (n : ℕ) (d : D n), IsAffineMap ℝ fun x => f n x d
n✝ : ℕ
n_ih✝ :
  (Nat.recOn n✝ x₀ fun n x => (r n).𝔼 (f n x)) =
    mean
      (Nat.recOn n✝ (pure x₀) fun n x => do
        let x' ← x
        let y' ← r n
        pure (f n x' y'))
⊢ (Nat.recOn (Nat.succ n✝) x₀ fun n x => (r n).𝔼 (f n x)) =
    mean
      (Nat.recOn (Nat.succ n✝) (pure x₀) fun n x => do
        let x' ← x
        let y' ← r n
        pure (f n x' y'))
Theorem: SciLean.Rand.pull_E_nat_recOn
Proof state before:
R : Type ?u.59471
inst✝¹³ : RealScalar R
X : Type ?u.59474
inst✝¹² : MeasurableSpace X
inst✝¹¹ : AddCommGroup X
inst✝¹⁰ : Module ℝ X
Y : Type ?u.60079
inst✝⁹ : AddCommGroup Y
inst✝⁸ : Module ℝ Y
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.60683
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module ℝ Z
C : ℕ → Type
inst✝⁴ : (n : ℕ) → AddCommGroup (C n)
inst✝³ : (n : ℕ) → Module ℝ (C n)
inst✝² : (n : ℕ) → MeasurableSpace (C n)
D : ℕ → Type
inst✝¹ inst✝ : (n : ℕ) → MeasurableSpace (D n)
x₀ : C 0
r : (n : ℕ) → Rand (D n)
f : (n : ℕ) → C n → D n → C (n + 1)
hf : ∀ (n : ℕ) (d : D n), IsAffineMap ℝ fun x => f n x d
⊢ (Nat.recOn Nat.zero x₀ fun n x => (r n).𝔼 (f n x)) =
    mean
      (Nat.recOn Nat.zero (pure x₀) fun n x => do
        let x' ← x
        let y' ← r n
        pure (f n x' y'))
Tactic:
case zero => simp[mean]
Proof state after:
no goals