Theorem: Probly.dflip_expectedValueChange (Probly/Flip.lean)

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]
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

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
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

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
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

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]
State after:
no goals