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

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

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

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

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
n : ℕ
hn :
  (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'))
Tactic:
simp[hn,mean,map]
State after:
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 : ℕ
hn :
  (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'))
⊢ (r n).𝔼
      (f n
        ((Nat.rec (pure x₀)
              (fun n x => do
                let x' ← x
                let y' ← r n
                pure (f n x' y'))
              n).𝔼
          id)) =
    (do
          let x' ←
            Nat.rec (pure x₀)
                (fun n x => do
                  let x' ← x
                  let y' ← r n
                  pure (f n x' y'))
                n
          let y' ← r n
          pure (f n x' y')).𝔼
      id

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
n : ℕ
hn :
  (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'))
⊢ (r n).𝔼
      (f n
        ((Nat.rec (pure x₀)
              (fun n x => do
                let x' ← x
                let y' ← r n
                pure (f n x' y'))
              n).𝔼
          id)) =
    (do
          let x' ←
            Nat.rec (pure x₀)
                (fun n x => do
                  let x' ← x
                  let y' ← r n
                  pure (f n x' y'))
                n
          let y' ← r n
          pure (f n x' y')).𝔼
      id
Tactic:
conv => simp[rand_pull_E,map]
State after:
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 : ℕ
hn :
  (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'))
⊢ (mean do
      let x' ← r n
      pure
          (f n
            (mean
              (Nat.rec (pure x₀)
                (fun n x => do
                  let x' ← x
                  let y' ← r n
                  pure (f n x' y'))
                n))
            x')) =
    mean do
      let x' ←
        Nat.rec (pure x₀)
            (fun n x => do
              let x' ← x
              let y' ← r n
              pure (f n x' y'))
            n
      let y' ← r n
      pure (f n x' y')

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
n : ℕ
hn :
  (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'))
⊢ (mean do
      let x' ← r n
      pure
          ((Nat.rec (pure x₀)
                (fun n x => do
                  let x' ← x
                  let y' ← r n
                  pure (f n x' y'))
                n).𝔼
            fun x => f n x x')) =
    mean do
      let x' ←
        Nat.rec (pure x₀)
            (fun n x => do
              let x' ← x
              let y' ← r n
              pure (f n x' y'))
            n
      let y' ← r n
      pure (f n x' y')
Tactic:
conv =>
  simp[rand_pull_E]
State after:
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 : ℕ
hn :
  (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'))
⊢ (mean do
      let x' ← r n
      (Nat.rec (pure x₀)
              (fun n x => do
                let x' ← x
                let y' ← r n
                pure (f n x' y'))
              n).map
          fun x => f n x x') =
    mean do
      let x' ←
        Nat.rec (pure x₀)
            (fun n x => do
              let x' ← x
              let y' ← r n
              pure (f n x' y'))
            n
      let y' ← r n
      pure (f n x' y')

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
n : ℕ
hn :
  (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'))
⊢ (mean do
      let x' ← r n
      (Nat.rec (pure x₀)
              (fun n x => do
                let x' ← x
                let y' ← r n
                pure (f n x' y'))
              n).map
          fun x => f n x x') =
    mean do
      let x' ←
        Nat.rec (pure x₀)
            (fun n x => do
              let x' ← x
              let y' ← r n
              pure (f n x' y'))
            n
      let y' ← r n
      pure (f n x' y')
Tactic:
rw[Rand.swap_bind]
State after:
no goals