Theorem: SciLean.Rand.pull_E_list_recOn (SciLean/Core/Rand/PushPullExpectation.lean)

State before:
R : Type ?u.82718
inst✝¹² : RealScalar R
X : Type ?u.82721
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module ℝ X
Y : Type ?u.83326
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.83930
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
α : Type u_1
C : List α → Type
inst✝³ : (n : List α) → AddCommGroup (C n)
inst✝² : (n : List α) → Module ℝ (C n)
inst✝¹ : (n : List α) → MeasurableSpace (C n)
D : List α → Type
inst✝ : (n : List α) → MeasurableSpace (D n)
l : List α
x₀ : C []
r : (head : α) → (tail : List α) → Rand (D (head :: tail))
f : (head : α) → (tail : List α) → C tail → D (head :: tail) → C (head :: tail)
hf : ∀ (head : α) (tail : List α) (d : D (head :: tail)), IsAffineMap ℝ fun x => f head tail x d
⊢ (List.recOn l x₀ fun head tail x => (r head tail).𝔼 (f head tail x)) =
    mean
      (List.recOn l (pure x₀) fun head tail x => do
        let x' ← x
        let y' ← r head tail
        pure (f head tail x' y'))
Tactic:
induction l
State after:
case nil
R : Type ?u.82718
inst✝¹² : RealScalar R
X : Type ?u.82721
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module ℝ X
Y : Type ?u.83326
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.83930
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
α : Type u_1
C : List α → Type
inst✝³ : (n : List α) → AddCommGroup (C n)
inst✝² : (n : List α) → Module ℝ (C n)
inst✝¹ : (n : List α) → MeasurableSpace (C n)
D : List α → Type
inst✝ : (n : List α) → MeasurableSpace (D n)
x₀ : C []
r : (head : α) → (tail : List α) → Rand (D (head :: tail))
f : (head : α) → (tail : List α) → C tail → D (head :: tail) → C (head :: tail)
hf : ∀ (head : α) (tail : List α) (d : D (head :: tail)), IsAffineMap ℝ fun x => f head tail x d
⊢ (List.recOn [] x₀ fun head tail x => (r head tail).𝔼 (f head tail x)) =
    mean
      (List.recOn [] (pure x₀) fun head tail x => do
        let x' ← x
        let y' ← r head tail
        pure (f head tail x' y'))

case cons
R : Type ?u.82718
inst✝¹² : RealScalar R
X : Type ?u.82721
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module ℝ X
Y : Type ?u.83326
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.83930
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
α : Type u_1
C : List α → Type
inst✝³ : (n : List α) → AddCommGroup (C n)
inst✝² : (n : List α) → Module ℝ (C n)
inst✝¹ : (n : List α) → MeasurableSpace (C n)
D : List α → Type
inst✝ : (n : List α) → MeasurableSpace (D n)
x₀ : C []
r : (head : α) → (tail : List α) → Rand (D (head :: tail))
f : (head : α) → (tail : List α) → C tail → D (head :: tail) → C (head :: tail)
hf : ∀ (head : α) (tail : List α) (d : D (head :: tail)), IsAffineMap ℝ fun x => f head tail x d
head✝ : α
tail✝ : List α
tail_ih✝ :
  (List.recOn tail✝ x₀ fun head tail x => (r head tail).𝔼 (f head tail x)) =
    mean
      (List.recOn tail✝ (pure x₀) fun head tail x => do
        let x' ← x
        let y' ← r head tail
        pure (f head tail x' y'))
⊢ (List.recOn (head✝ :: tail✝) x₀ fun head tail x => (r head tail).𝔼 (f head tail x)) =
    mean
      (List.recOn (head✝ :: tail✝) (pure x₀) fun head tail x => do
        let x' ← x
        let y' ← r head tail
        pure (f head tail x' y'))

State before:
R : Type ?u.82718
inst✝¹² : RealScalar R
X : Type ?u.82721
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module ℝ X
Y : Type ?u.83326
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.83930
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
α : Type u_1
C : List α → Type
inst✝³ : (n : List α) → AddCommGroup (C n)
inst✝² : (n : List α) → Module ℝ (C n)
inst✝¹ : (n : List α) → MeasurableSpace (C n)
D : List α → Type
inst✝ : (n : List α) → MeasurableSpace (D n)
x₀ : C []
r : (head : α) → (tail : List α) → Rand (D (head :: tail))
f : (head : α) → (tail : List α) → C tail → D (head :: tail) → C (head :: tail)
hf : ∀ (head : α) (tail : List α) (d : D (head :: tail)), IsAffineMap ℝ fun x => f head tail x d
⊢ (List.recOn [] x₀ fun head tail x => (r head tail).𝔼 (f head tail x)) =
    mean
      (List.recOn [] (pure x₀) fun head tail x => do
        let x' ← x
        let y' ← r head tail
        pure (f head tail x' y'))
Tactic:
case nil => simp[mean]
State after:
no goals

State before:
R : Type ?u.82718
inst✝¹² : RealScalar R
X : Type ?u.82721
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module ℝ X
Y : Type ?u.83326
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.83930
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
α : Type u_1
C : List α → Type
inst✝³ : (n : List α) → AddCommGroup (C n)
inst✝² : (n : List α) → Module ℝ (C n)
inst✝¹ : (n : List α) → MeasurableSpace (C n)
D : List α → Type
inst✝ : (n : List α) → MeasurableSpace (D n)
x₀ : C []
r : (head : α) → (tail : List α) → Rand (D (head :: tail))
f : (head : α) → (tail : List α) → C tail → D (head :: tail) → C (head :: tail)
hf : ∀ (head : α) (tail : List α) (d : D (head :: tail)), IsAffineMap ℝ fun x => f head tail x d
⊢ (List.recOn [] x₀ fun head tail x => (r head tail).𝔼 (f head tail x)) =
    mean
      (List.recOn [] (pure x₀) fun head tail x => do
        let x' ← x
        let y' ← r head tail
        pure (f head tail x' y'))
Tactic:
simp[mean]
State after:
no goals

State before:
R : Type ?u.82718
inst✝¹² : RealScalar R
X : Type ?u.82721
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module ℝ X
Y : Type ?u.83326
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.83930
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
α : Type u_1
C : List α → Type
inst✝³ : (n : List α) → AddCommGroup (C n)
inst✝² : (n : List α) → Module ℝ (C n)
inst✝¹ : (n : List α) → MeasurableSpace (C n)
D : List α → Type
inst✝ : (n : List α) → MeasurableSpace (D n)
x₀ : C []
r : (head : α) → (tail : List α) → Rand (D (head :: tail))
f : (head : α) → (tail : List α) → C tail → D (head :: tail) → C (head :: tail)
hf : ∀ (head : α) (tail : List α) (d : D (head :: tail)), IsAffineMap ℝ fun x => f head tail x d
head : α
tail : List α
hn :
  (List.recOn tail x₀ fun head tail x => (r head tail).𝔼 (f head tail x)) =
    mean
      (List.recOn tail (pure x₀) fun head tail x => do
        let x' ← x
        let y' ← r head tail
        pure (f head tail x' y'))
⊢ (List.recOn (head :: tail) x₀ fun head tail x => (r head tail).𝔼 (f head tail x)) =
    mean
      (List.recOn (head :: tail) (pure x₀) fun head tail x => do
        let x' ← x
        let y' ← r head tail
        pure (f head tail x' y'))
Tactic:
simp[hn,mean]
State after:
R : Type ?u.82718
inst✝¹² : RealScalar R
X : Type ?u.82721
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module ℝ X
Y : Type ?u.83326
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.83930
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
α : Type u_1
C : List α → Type
inst✝³ : (n : List α) → AddCommGroup (C n)
inst✝² : (n : List α) → Module ℝ (C n)
inst✝¹ : (n : List α) → MeasurableSpace (C n)
D : List α → Type
inst✝ : (n : List α) → MeasurableSpace (D n)
x₀ : C []
r : (head : α) → (tail : List α) → Rand (D (head :: tail))
f : (head : α) → (tail : List α) → C tail → D (head :: tail) → C (head :: tail)
hf : ∀ (head : α) (tail : List α) (d : D (head :: tail)), IsAffineMap ℝ fun x => f head tail x d
head : α
tail : List α
hn :
  (List.recOn tail x₀ fun head tail x => (r head tail).𝔼 (f head tail x)) =
    mean
      (List.recOn tail (pure x₀) fun head tail x => do
        let x' ← x
        let y' ← r head tail
        pure (f head tail x' y'))
⊢ (r head tail).𝔼
      (f head tail
        ((List.rec (pure x₀)
              (fun head tail x => do
                let x' ← x
                let y' ← r head tail
                pure (f head tail x' y'))
              tail).𝔼
          id)) =
    (do
          let x' ←
            List.rec (pure x₀)
                (fun head tail x => do
                  let x' ← x
                  let y' ← r head tail
                  pure (f head tail x' y'))
                tail
          let y' ← r head tail
          pure (f head tail x' y')).𝔼
      id

State before:
R : Type ?u.82718
inst✝¹² : RealScalar R
X : Type ?u.82721
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module ℝ X
Y : Type ?u.83326
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.83930
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
α : Type u_1
C : List α → Type
inst✝³ : (n : List α) → AddCommGroup (C n)
inst✝² : (n : List α) → Module ℝ (C n)
inst✝¹ : (n : List α) → MeasurableSpace (C n)
D : List α → Type
inst✝ : (n : List α) → MeasurableSpace (D n)
x₀ : C []
r : (head : α) → (tail : List α) → Rand (D (head :: tail))
f : (head : α) → (tail : List α) → C tail → D (head :: tail) → C (head :: tail)
hf : ∀ (head : α) (tail : List α) (d : D (head :: tail)), IsAffineMap ℝ fun x => f head tail x d
head : α
tail : List α
hn :
  (List.recOn tail x₀ fun head tail x => (r head tail).𝔼 (f head tail x)) =
    mean
      (List.recOn tail (pure x₀) fun head tail x => do
        let x' ← x
        let y' ← r head tail
        pure (f head tail x' y'))
⊢ (r head tail).𝔼
      (f head tail
        ((List.rec (pure x₀)
              (fun head tail x => do
                let x' ← x
                let y' ← r head tail
                pure (f head tail x' y'))
              tail).𝔼
          id)) =
    (do
          let x' ←
            List.rec (pure x₀)
                (fun head tail x => do
                  let x' ← x
                  let y' ← r head tail
                  pure (f head tail x' y'))
                tail
          let y' ← r head tail
          pure (f head tail x' y')).𝔼
      id
Tactic:
conv => simp[rand_pull_E,map]
State after:
R : Type ?u.82718
inst✝¹² : RealScalar R
X : Type ?u.82721
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module ℝ X
Y : Type ?u.83326
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.83930
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
α : Type u_1
C : List α → Type
inst✝³ : (n : List α) → AddCommGroup (C n)
inst✝² : (n : List α) → Module ℝ (C n)
inst✝¹ : (n : List α) → MeasurableSpace (C n)
D : List α → Type
inst✝ : (n : List α) → MeasurableSpace (D n)
x₀ : C []
r : (head : α) → (tail : List α) → Rand (D (head :: tail))
f : (head : α) → (tail : List α) → C tail → D (head :: tail) → C (head :: tail)
hf : ∀ (head : α) (tail : List α) (d : D (head :: tail)), IsAffineMap ℝ fun x => f head tail x d
head : α
tail : List α
hn :
  (List.recOn tail x₀ fun head tail x => (r head tail).𝔼 (f head tail x)) =
    mean
      (List.recOn tail (pure x₀) fun head tail x => do
        let x' ← x
        let y' ← r head tail
        pure (f head tail x' y'))
⊢ (mean do
      let x' ← r head tail
      pure
          (f head tail
            (mean
              (List.rec (pure x₀)
                (fun head tail x => do
                  let x' ← x
                  let y' ← r head tail
                  pure (f head tail x' y'))
                tail))
            x')) =
    mean do
      let x' ←
        List.rec (pure x₀)
            (fun head tail x => do
              let x' ← x
              let y' ← r head tail
              pure (f head tail x' y'))
            tail
      let y' ← r head tail
      pure (f head tail x' y')

State before:
R : Type ?u.82718
inst✝¹² : RealScalar R
X : Type ?u.82721
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module ℝ X
Y : Type ?u.83326
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.83930
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
α : Type u_1
C : List α → Type
inst✝³ : (n : List α) → AddCommGroup (C n)
inst✝² : (n : List α) → Module ℝ (C n)
inst✝¹ : (n : List α) → MeasurableSpace (C n)
D : List α → Type
inst✝ : (n : List α) → MeasurableSpace (D n)
x₀ : C []
r : (head : α) → (tail : List α) → Rand (D (head :: tail))
f : (head : α) → (tail : List α) → C tail → D (head :: tail) → C (head :: tail)
hf : ∀ (head : α) (tail : List α) (d : D (head :: tail)), IsAffineMap ℝ fun x => f head tail x d
head : α
tail : List α
hn :
  (List.recOn tail x₀ fun head tail x => (r head tail).𝔼 (f head tail x)) =
    mean
      (List.recOn tail (pure x₀) fun head tail x => do
        let x' ← x
        let y' ← r head tail
        pure (f head tail x' y'))
⊢ (mean do
      let x' ← r head tail
      pure
          ((List.rec (pure x₀)
                (fun head tail x => do
                  let x' ← x
                  let y' ← r head tail
                  pure (f head tail x' y'))
                tail).𝔼
            fun x => f head tail x x')) =
    mean do
      let x' ←
        List.rec (pure x₀)
            (fun head tail x => do
              let x' ← x
              let y' ← r head tail
              pure (f head tail x' y'))
            tail
      let y' ← r head tail
      pure (f head tail x' y')
Tactic:
conv =>
  simp[rand_pull_E]
State after:
R : Type ?u.82718
inst✝¹² : RealScalar R
X : Type ?u.82721
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module ℝ X
Y : Type ?u.83326
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.83930
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
α : Type u_1
C : List α → Type
inst✝³ : (n : List α) → AddCommGroup (C n)
inst✝² : (n : List α) → Module ℝ (C n)
inst✝¹ : (n : List α) → MeasurableSpace (C n)
D : List α → Type
inst✝ : (n : List α) → MeasurableSpace (D n)
x₀ : C []
r : (head : α) → (tail : List α) → Rand (D (head :: tail))
f : (head : α) → (tail : List α) → C tail → D (head :: tail) → C (head :: tail)
hf : ∀ (head : α) (tail : List α) (d : D (head :: tail)), IsAffineMap ℝ fun x => f head tail x d
head : α
tail : List α
hn :
  (List.recOn tail x₀ fun head tail x => (r head tail).𝔼 (f head tail x)) =
    mean
      (List.recOn tail (pure x₀) fun head tail x => do
        let x' ← x
        let y' ← r head tail
        pure (f head tail x' y'))
⊢ (mean do
      let x' ← r head tail
      (List.rec (pure x₀)
              (fun head tail x => do
                let x' ← x
                let y' ← r head tail
                pure (f head tail x' y'))
              tail).map
          fun x => f head tail x x') =
    mean do
      let x' ←
        List.rec (pure x₀)
            (fun head tail x => do
              let x' ← x
              let y' ← r head tail
              pure (f head tail x' y'))
            tail
      let y' ← r head tail
      pure (f head tail x' y')

State before:
R : Type ?u.82718
inst✝¹² : RealScalar R
X : Type ?u.82721
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module ℝ X
Y : Type ?u.83326
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.83930
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
α : Type u_1
C : List α → Type
inst✝³ : (n : List α) → AddCommGroup (C n)
inst✝² : (n : List α) → Module ℝ (C n)
inst✝¹ : (n : List α) → MeasurableSpace (C n)
D : List α → Type
inst✝ : (n : List α) → MeasurableSpace (D n)
x₀ : C []
r : (head : α) → (tail : List α) → Rand (D (head :: tail))
f : (head : α) → (tail : List α) → C tail → D (head :: tail) → C (head :: tail)
hf : ∀ (head : α) (tail : List α) (d : D (head :: tail)), IsAffineMap ℝ fun x => f head tail x d
head : α
tail : List α
hn :
  (List.recOn tail x₀ fun head tail x => (r head tail).𝔼 (f head tail x)) =
    mean
      (List.recOn tail (pure x₀) fun head tail x => do
        let x' ← x
        let y' ← r head tail
        pure (f head tail x' y'))
⊢ (mean do
      let x' ← r head tail
      (List.rec (pure x₀)
              (fun head tail x => do
                let x' ← x
                let y' ← r head tail
                pure (f head tail x' y'))
              tail).map
          fun x => f head tail x x') =
    mean do
      let x' ←
        List.rec (pure x₀)
            (fun head tail x => do
              let x' ← x
              let y' ← r head tail
              pure (f head tail x' y'))
            tail
      let y' ← r head tail
      pure (f head tail x' y')
Tactic:
rw[Rand.swap_bind]
State after:
no goals