internlm/Lean-Github huggingface dataset:
Theorem: Probly.dflip_expectedValueChange
Proof state before:
W : Type ?u.18771
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.19006
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.19123
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.19240
inst✝¹ : MeasurableSpace α
β : Type ?u.19246
inst✝ : MeasurableSpace β
f : Bool → X
⊢ DRand.dE dflip f = f true - f false
Tactic:
simp [DRand.dE,dflip]
Proof state after:
W : Type ?u.18771
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.19006
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.19123
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.19240
inst✝¹ : MeasurableSpace α
β : Type ?u.19246
inst✝ : MeasurableSpace β
f : Bool → X
⊢ testFunctionExtension (fun φ => φ true - φ false) f = f true - f false
Theorem: Probly.dflip_expectedValueChange
Proof state before:
W : Type ?u.18771
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.19006
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.19123
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.19240
inst✝¹ : MeasurableSpace α
β : Type ?u.19246
inst✝ : MeasurableSpace β
f : Bool → X
⊢ testFunctionExtension (fun φ => φ true - φ false) f = f true - f false
Tactic:
apply testFunctionExtension_ext
Proof state after:
case h
W : Type ?u.18771
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.19006
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.19123
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.19240
inst✝¹ : MeasurableSpace α
β : Type ?u.19246
inst✝ : MeasurableSpace β
f : Bool → X
⊢ ∀ (φ : Bool → ℝ) (y : X), (φ true - φ false) • y = (fun x => φ x • y) true - (fun x => φ x • y) false
Theorem: Probly.dflip_expectedValueChange
Proof state before:
case h
W : Type ?u.18771
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.19006
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.19123
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.19240
inst✝¹ : MeasurableSpace α
β : Type ?u.19246
inst✝ : MeasurableSpace β
f : Bool → X
⊢ ∀ (φ : Bool → ℝ) (y : X), (φ true - φ false) • y = (fun x => φ x • y) true - (fun x => φ x • y) false
Tactic:
intro φ y
Proof state after:
case h
W : Type ?u.18771
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.19006
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.19123
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.19240
inst✝¹ : MeasurableSpace α
β : Type ?u.19246
inst✝ : MeasurableSpace β
f : Bool → X
φ : Bool → ℝ
y : X
⊢ (φ true - φ false) • y = (fun x => φ x • y) true - (fun x => φ x • y) false
Theorem: Probly.dflip_expectedValueChange
Proof state before:
case h
W : Type ?u.18771
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.19006
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.19123
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.19240
inst✝¹ : MeasurableSpace α
β : Type ?u.19246
inst✝ : MeasurableSpace β
f : Bool → X
φ : Bool → ℝ
y : X
⊢ (φ true - φ false) • y = (fun x => φ x • y) true - (fun x => φ x • y) false
Tactic:
simp [sub_smul]
Proof state after:
no goals
Theorem: Probly.flip.arg_x.randDeriv_rule
Proof state before:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.21696
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21813
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21930
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.22047
inst✝¹ : MeasurableSpace α
β : Type ?u.22053
inst✝ : MeasurableSpace β
x : W → ℝ
hf : Differentiable ℝ x
⊢ (randDeriv fun w => flip (x w)) = fun w dw =>
    let dx' := (fderiv ℝ x w) dw;
    dx' • dflip
Tactic:
simp (disch:=sorry) [rand_simp]
Proof state after:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.21696
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21813
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21930
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.22047
inst✝¹ : MeasurableSpace α
β : Type ?u.22053
inst✝ : MeasurableSpace β
x : W → ℝ
hf : Differentiable ℝ x
⊢ (fun x_1 dx => randDeriv flip (x x_1) ((fderiv ℝ (fun x_2 => x x_2) x_1) dx)) = fun w dw => (fderiv ℝ x w) dw • dflip
Theorem: Probly.flip.arg_x.randDeriv_rule
Proof state before:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.21696
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21813
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21930
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.22047
inst✝¹ : MeasurableSpace α
β : Type ?u.22053
inst✝ : MeasurableSpace β
x : W → ℝ
hf : Differentiable ℝ x
⊢ (fun x_1 dx => randDeriv flip (x x_1) ((fderiv ℝ (fun x_2 => x x_2) x_1) dx)) = fun w dw => (fderiv ℝ x w) dw • dflip
Tactic:
funext w dw
Proof state after:
case h.h
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.21696
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21813
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21930
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.22047
inst✝¹ : MeasurableSpace α
β : Type ?u.22053
inst✝ : MeasurableSpace β
x : W → ℝ
hf : Differentiable ℝ x
w dw : W
⊢ randDeriv flip (x w) ((fderiv ℝ (fun x_1 => x x_1) w) dw) = (fderiv ℝ x w) dw • dflip
Theorem: Probly.flip.arg_x.randDeriv_rule
Proof state before:
case h.h
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.21696
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21813
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21930
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.22047
inst✝¹ : MeasurableSpace α
β : Type ?u.22053
inst✝ : MeasurableSpace β
x : W → ℝ
hf : Differentiable ℝ x
w dw : W
⊢ randDeriv flip (x w) ((fderiv ℝ (fun x_1 => x x_1) w) dw) = (fderiv ℝ x w) dw • dflip
Tactic:
simp [randDeriv]
Proof state after:
case h.h
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.21696
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21813
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21930
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.22047
inst✝¹ : MeasurableSpace α
β : Type ?u.22053
inst✝ : MeasurableSpace β
x : W → ℝ
hf : Differentiable ℝ x
w dw : W
⊢ {
      action := fun φ =>
        (fderiv ℝ (fun x' => x' * φ true + (1 - x') * φ false) (x w)) ((fderiv ℝ (fun x_1 => x x_1) w) dw) } =
    (fderiv ℝ x w) dw • dflip
Theorem: Probly.flip.arg_x.randDeriv_rule
Proof state before:
case h.h
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.21696
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21813
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21930
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.22047
inst✝¹ : MeasurableSpace α
β : Type ?u.22053
inst✝ : MeasurableSpace β
x : W → ℝ
hf : Differentiable ℝ x
w dw : W
⊢ {
      action := fun φ =>
        (fderiv ℝ (fun x' => x' * φ true + (1 - x') * φ false) (x w)) ((fderiv ℝ (fun x_1 => x x_1) w) dw) } =
    (fderiv ℝ x w) dw • dflip
Tactic:
apply DRand.ext
Proof state after:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.21696
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21813
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21930
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.22047
inst✝¹ : MeasurableSpace α
β : Type ?u.22053
inst✝ : MeasurableSpace β
x : W → ℝ
hf : Differentiable ℝ x
w dw : W
⊢ ∀ (φ : Bool → ℝ),
    {
            action := fun φ =>
              (fderiv ℝ (fun x' => x' * φ true + (1 - x') * φ false) (x w))
                ((fderiv ℝ (fun x_1 => x x_1) w) dw) }.action
        φ =
      ((fderiv ℝ x w) dw • dflip).action φ
Theorem: Probly.flip.arg_x.randDeriv_rule
Proof state before:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.21696
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21813
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21930
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.22047
inst✝¹ : MeasurableSpace α
β : Type ?u.22053
inst✝ : MeasurableSpace β
x : W → ℝ
hf : Differentiable ℝ x
w dw : W
⊢ ∀ (φ : Bool → ℝ),
    {
            action := fun φ =>
              (fderiv ℝ (fun x' => x' * φ true + (1 - x') * φ false) (x w))
                ((fderiv ℝ (fun x_1 => x x_1) w) dw) }.action
        φ =
      ((fderiv ℝ x w) dw • dflip).action φ
Tactic:
intro φ
Proof state after:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.21696
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21813
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21930
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.22047
inst✝¹ : MeasurableSpace α
β : Type ?u.22053
inst✝ : MeasurableSpace β
x : W → ℝ
hf : Differentiable ℝ x
w dw : W
φ : Bool → ℝ
⊢ {
          action := fun φ =>
            (fderiv ℝ (fun x' => x' * φ true + (1 - x') * φ false) (x w)) ((fderiv ℝ (fun x_1 => x x_1) w) dw) }.action
      φ =
    ((fderiv ℝ x w) dw • dflip).action φ
Theorem: Probly.flip.arg_x.randDeriv_rule
Proof state before:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.21696
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21813
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21930
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.22047
inst✝¹ : MeasurableSpace α
β : Type ?u.22053
inst✝ : MeasurableSpace β
x : W → ℝ
hf : Differentiable ℝ x
w dw : W
φ : Bool → ℝ
⊢ {
          action := fun φ =>
            (fderiv ℝ (fun x' => x' * φ true + (1 - x') * φ false) (x w)) ((fderiv ℝ (fun x_1 => x x_1) w) dw) }.action
      φ =
    ((fderiv ℝ x w) dw • dflip).action φ
Tactic:
simp[dflip,rand_simp]
Proof state after:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.21696
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21813
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21930
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.22047
inst✝¹ : MeasurableSpace α
β : Type ?u.22053
inst✝ : MeasurableSpace β
x : W → ℝ
hf : Differentiable ℝ x
w dw : W
φ : Bool → ℝ
⊢ (fderiv ℝ (fun x' => x' * φ true + (1 - x') * φ false) (x w)) ((fderiv ℝ (fun x_1 => x x_1) w) dw) =
    (fderiv ℝ x w) dw * (φ true - φ false)
Theorem: Probly.flip.arg_x.randDeriv_rule
Proof state before:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.21696
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21813
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21930
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.22047
inst✝¹ : MeasurableSpace α
β : Type ?u.22053
inst✝ : MeasurableSpace β
x : W → ℝ
hf : Differentiable ℝ x
w dw : W
φ : Bool → ℝ
⊢ (fderiv ℝ (fun x' => x' * φ true + (1 - x') * φ false) (x w)) ((fderiv ℝ (fun x_1 => x x_1) w) dw) =
    (fderiv ℝ x w) dw * (φ true - φ false)
Tactic:
sorry
Proof state after:
no goals
Theorem: Probly.flip.arg_x.randFwdDeriv_rule
Proof state before:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.33480
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.33597
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.33714
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.33831
inst✝¹ : MeasurableSpace α
β : Type ?u.33837
inst✝ : MeasurableSpace β
x : W → ℝ
hf : Differentiable ℝ x
⊢ (randFwdDeriv fun w => flip (x w)) = fun w dw =>
    let x' := x w;
    let dx' := (fderiv ℝ x w) dw;
    { val := flip x', dval := dx' • dflip }
Tactic:
unfold randFwdDeriv
Proof state after:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.33480
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.33597
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.33714
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.33831
inst✝¹ : MeasurableSpace α
β : Type ?u.33837
inst✝ : MeasurableSpace β
x : W → ℝ
hf : Differentiable ℝ x
⊢ (fun x_1 dx => { val := (fun w => flip (x w)) x_1, dval := randDeriv (fun w => flip (x w)) x_1 dx }) = fun w dw =>
    let x' := x w;
    let dx' := (fderiv ℝ x w) dw;
    { val := flip x', dval := dx' • dflip }
Theorem: Probly.flip.arg_x.randFwdDeriv_rule
Proof state before:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.33480
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.33597
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.33714
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.33831
inst✝¹ : MeasurableSpace α
β : Type ?u.33837
inst✝ : MeasurableSpace β
x : W → ℝ
hf : Differentiable ℝ x
⊢ (fun x_1 dx => { val := (fun w => flip (x w)) x_1, dval := randDeriv (fun w => flip (x w)) x_1 dx }) = fun w dw =>
    let x' := x w;
    let dx' := (fderiv ℝ x w) dw;
    { val := flip x', dval := dx' • dflip }
Tactic:
simp (disch:= first | apply hf | sorry) [rand_simp]
Proof state after:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.33480
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.33597
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.33714
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.33831
inst✝¹ : MeasurableSpace α
β : Type ?u.33837
inst✝ : MeasurableSpace β
x : W → ℝ
hf : Differentiable ℝ x
⊢ (fun x_1 dx => { val := flip (x x_1), dval := randDeriv flip (x x_1) ((fderiv ℝ (fun x_2 => x x_2) x_1) dx) }) =
    fun w dw => { val := flip (x w), dval := (fderiv ℝ x w) dw • dflip }
Theorem: Probly.flip.arg_x.randFwdDeriv_rule
Proof state before:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.33480
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.33597
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.33714
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.33831
inst✝¹ : MeasurableSpace α
β : Type ?u.33837
inst✝ : MeasurableSpace β
x : W → ℝ
hf : Differentiable ℝ x
⊢ (fun x_1 dx => { val := flip (x x_1), dval := randDeriv flip (x x_1) ((fderiv ℝ (fun x_2 => x x_2) x_1) dx) }) =
    fun w dw => { val := flip (x w), dval := (fderiv ℝ x w) dw • dflip }
Tactic:
rw[flip.arg_x.randDeriv_rule _ differentiable_id']
Proof state after:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.33480
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.33597
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.33714
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.33831
inst✝¹ : MeasurableSpace α
β : Type ?u.33837
inst✝ : MeasurableSpace β
x : W → ℝ
hf : Differentiable ℝ x
⊢ (fun x_1 dx =>
      { val := flip (x x_1),
        dval :=
          (fun w dw =>
              let dx' := (fderiv ℝ (fun x => x) w) dw;
              dx' • dflip)
            (x x_1) ((fderiv ℝ (fun x_2 => x x_2) x_1) dx) }) =
    fun w dw => { val := flip (x w), dval := (fderiv ℝ x w) dw • dflip }
Theorem: Probly.flip.arg_x.randFwdDeriv_rule
Proof state before:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.33480
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.33597
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.33714
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.33831
inst✝¹ : MeasurableSpace α
β : Type ?u.33837
inst✝ : MeasurableSpace β
x : W → ℝ
hf : Differentiable ℝ x
⊢ (fun x_1 dx =>
      { val := flip (x x_1),
        dval :=
          (fun w dw =>
              let dx' := (fderiv ℝ (fun x => x) w) dw;
              dx' • dflip)
            (x x_1) ((fderiv ℝ (fun x_2 => x x_2) x_1) dx) }) =
    fun w dw => { val := flip (x w), dval := (fderiv ℝ x w) dw • dflip }
Tactic:
simp
Proof state after:
no goals
Theorem: Probly.flip.arg_x.randFwdDeriv_rule_siple
Proof state before:
W : Type ?u.42250
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.42368
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.42485
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.42602
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.42719
inst✝¹ : MeasurableSpace α
β : Type ?u.42725
inst✝ : MeasurableSpace β
⊢ (randFwdDeriv fun x => flip x) = fun x dx => { val := flip x, dval := dx • dflip }
Tactic:
unfold randFwdDeriv
Proof state after:
W : Type ?u.42250
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.42368
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.42485
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.42602
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.42719
inst✝¹ : MeasurableSpace α
β : Type ?u.42725
inst✝ : MeasurableSpace β
⊢ (fun x dx => { val := (fun x => flip x) x, dval := randDeriv (fun x => flip x) x dx }) = fun x dx =>
    { val := flip x, dval := dx • dflip }
Theorem: Probly.flip.arg_x.randFwdDeriv_rule_siple
Proof state before:
W : Type ?u.42250
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.42368
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.42485
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.42602
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.42719
inst✝¹ : MeasurableSpace α
β : Type ?u.42725
inst✝ : MeasurableSpace β
⊢ (fun x dx => { val := (fun x => flip x) x, dval := randDeriv (fun x => flip x) x dx }) = fun x dx =>
    { val := flip x, dval := dx • dflip }
Tactic:
simp (disch:= first | apply hf | sorry) [rand_simp]
Proof state after:
W : Type ?u.42250
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.42368
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.42485
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.42602
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.42719
inst✝¹ : MeasurableSpace α
β : Type ?u.42725
inst✝ : MeasurableSpace β
⊢ (fun x dx => { val := flip x, dval := randDeriv (fun x => flip x) x dx }) = fun x dx =>
    { val := flip x, dval := dx • dflip }
Theorem: Probly.flip.arg_x.randFwdDeriv_rule_siple
Proof state before:
W : Type ?u.42250
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.42368
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.42485
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.42602
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.42719
inst✝¹ : MeasurableSpace α
β : Type ?u.42725
inst✝ : MeasurableSpace β
⊢ (fun x dx => { val := flip x, dval := randDeriv (fun x => flip x) x dx }) = fun x dx =>
    { val := flip x, dval := dx • dflip }
Tactic:
rw[flip.arg_x.randDeriv_rule _ differentiable_id']
Proof state after:
W : Type ?u.42250
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.42368
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.42485
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.42602
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.42719
inst✝¹ : MeasurableSpace α
β : Type ?u.42725
inst✝ : MeasurableSpace β
⊢ (fun x dx =>
      { val := flip x,
        dval :=
          (fun w dw =>
              let dx' := (fderiv ℝ (fun x => x) w) dw;
              dx' • dflip)
            x dx }) =
    fun x dx => { val := flip x, dval := dx • dflip }