internlm/Lean-Github huggingface dataset:
Theorem: SciLean.explicitSymplecticEuler_eq_implicitSymplecticEulerV1
Proof state before:
R : Type u_1
inst✝⁶ : RCLike R
X✝ : Type ?u.46671
inst✝⁵ : Vec R X✝
Y✝ : Type ?u.46685
inst✝⁴ : Vec R Y✝
Z✝ : Type ?u.46697
inst✝³ : Vec R Z✝
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.46721
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.46733
inst✝ : SemiInnerProductSpace R Z
T V : X → R
hT : HasAdjDiff R T
hV : HasAdjDiff R V
⊢ (explicitSymplecticEuler fun q p => T p + V q) = implicitSymplecticEulerV1 fun q p => T p + V q
Tactic:
unfold implicitSymplecticEulerV1
Proof state after:
R : Type u_1
inst✝⁶ : RCLike R
X✝ : Type ?u.46671
inst✝⁵ : Vec R X✝
Y✝ : Type ?u.46685
inst✝⁴ : Vec R Y✝
Z✝ : Type ?u.46697
inst✝³ : Vec R Z✝
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.46721
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.46733
inst✝ : SemiInnerProductSpace R Z
T V : X → R
hT : HasAdjDiff R T
hV : HasAdjDiff R V
⊢ (explicitSymplecticEuler fun q p => T p + V q) = fun Δt qₙ pₙ =>
    solve q' p',
      q' = qₙ + Δt • ∇ (p:=p'), (fun q p => T p + V q) qₙ p ∧ p' = pₙ - Δt • ∇ (q:=qₙ), (fun q p => T p + V q) q p'
Theorem: SciLean.explicitSymplecticEuler_eq_implicitSymplecticEulerV1
Proof state before:
R : Type u_1
inst✝⁶ : RCLike R
X✝ : Type ?u.46671
inst✝⁵ : Vec R X✝
Y✝ : Type ?u.46685
inst✝⁴ : Vec R Y✝
Z✝ : Type ?u.46697
inst✝³ : Vec R Z✝
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.46721
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.46733
inst✝ : SemiInnerProductSpace R Z
T V : X → R
hT : HasAdjDiff R T
hV : HasAdjDiff R V
⊢ (explicitSymplecticEuler fun q p => T p + V q) = fun Δt qₙ pₙ =>
    solve q' p',
      q' = qₙ + Δt • ∇ (p:=p'), (fun q p => T p + V q) qₙ p ∧ p' = pₙ - Δt • ∇ (q:=qₙ), (fun q p => T p + V q) q p'
Tactic:
unfold explicitSymplecticEuler
Proof state after:
R : Type u_1
inst✝⁶ : RCLike R
X✝ : Type ?u.46671
inst✝⁵ : Vec R X✝
Y✝ : Type ?u.46685
inst✝⁴ : Vec R Y✝
Z✝ : Type ?u.46697
inst✝³ : Vec R Z✝
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.46721
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.46733
inst✝ : SemiInnerProductSpace R Z
T V : X → R
hT : HasAdjDiff R T
hV : HasAdjDiff R V
⊢ (fun Δt qₙ pₙ =>
      let p' := pₙ - Δt • ∇ (q:=qₙ), (fun q p => T p + V q) q pₙ;
      let q' := qₙ + Δt • ∇ (p:=p'), (fun q p => T p + V q) qₙ p;
      (q', p')) =
    fun Δt qₙ pₙ =>
    solve q' p',
      q' = qₙ + Δt • ∇ (p:=p'), (fun q p => T p + V q) qₙ p ∧ p' = pₙ - Δt • ∇ (q:=qₙ), (fun q p => T p + V q) q p'
Theorem: SciLean.explicitSymplecticEuler_eq_implicitSymplecticEulerV1
Proof state before:
R : Type u_1
inst✝⁶ : RCLike R
X✝ : Type ?u.46671
inst✝⁵ : Vec R X✝
Y✝ : Type ?u.46685
inst✝⁴ : Vec R Y✝
Z✝ : Type ?u.46697
inst✝³ : Vec R Z✝
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.46721
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.46733
inst✝ : SemiInnerProductSpace R Z
T V : X → R
hT : HasAdjDiff R T
hV : HasAdjDiff R V
⊢ (fun Δt qₙ pₙ =>
      let p' := pₙ - Δt • ∇ (q:=qₙ), (fun q p => T p + V q) q pₙ;
      let q' := qₙ + Δt • ∇ (p:=p'), (fun q p => T p + V q) qₙ p;
      (q', p')) =
    fun Δt qₙ pₙ =>
    solve q' p',
      q' = qₙ + Δt • ∇ (p:=p'), (fun q p => T p + V q) qₙ p ∧ p' = pₙ - Δt • ∇ (q:=qₙ), (fun q p => T p + V q) q p'
Tactic:
conv =>
  rhs
  solve_for p' from 1 := sorry_proof
  solve_as_inv
  solve_as_inv
Proof state after:
R : Type u_1
inst✝⁶ : RCLike R
X✝ : Type ?u.46671
inst✝⁵ : Vec R X✝
Y✝ : Type ?u.46685
inst✝⁴ : Vec R Y✝
Z✝ : Type ?u.46697
inst✝³ : Vec R Z✝
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.46721
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.46733
inst✝ : SemiInnerProductSpace R Z
T V : X → R
hT : HasAdjDiff R T
hV : HasAdjDiff R V
⊢ (fun Δt qₙ pₙ =>
      let p' := pₙ - Δt • ∇ (q:=qₙ), (fun q p => T p + V q) q pₙ;
      let q' := qₙ + Δt • ∇ (p:=p'), (fun q p => T p + V q) qₙ p;
      (q', p')) =
    fun Δt qₙ pₙ =>
    let p'' := fun q' => Function.invFun (fun x => x - (pₙ - Δt • ∇ (q:=qₙ), (T x + V q))) 0;
    let q' := Function.invFun (fun x => x - (qₙ + Δt • ∇ (p:=p'' x), (T p + V qₙ))) 0;
    let p' := p'' q';
    (q', p')
Theorem: SciLean.explicitSymplecticEuler_eq_implicitSymplecticEulerV1
Proof state before:
R : Type u_1
inst✝⁶ : RCLike R
X✝ : Type ?u.46671
inst✝⁵ : Vec R X✝
Y✝ : Type ?u.46685
inst✝⁴ : Vec R Y✝
Z✝ : Type ?u.46697
inst✝³ : Vec R Z✝
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.46721
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.46733
inst✝ : SemiInnerProductSpace R Z
T V : X → R
hT : HasAdjDiff R T
hV : HasAdjDiff R V
⊢ (fun Δt qₙ pₙ =>
      let p' := pₙ - Δt • ∇ (q:=qₙ), (fun q p => T p + V q) q pₙ;
      let q' := qₙ + Δt • ∇ (p:=p'), (fun q p => T p + V q) qₙ p;
      (q', p')) =
    fun Δt qₙ pₙ =>
    let p'' := fun q' => Function.invFun (fun x => x - (pₙ - Δt • ∇ (q:=qₙ), (T x + V q))) 0;
    let q' := Function.invFun (fun x => x - (qₙ + Δt • ∇ (p:=p'' x), (T p + V qₙ))) 0;
    let p' := p'' q';
    (q', p')
Tactic:
autodiff
Proof state after:
R : Type u_1
inst✝⁶ : RCLike R
X✝ : Type ?u.46671
inst✝⁵ : Vec R X✝
Y✝ : Type ?u.46685
inst✝⁴ : Vec R Y✝
Z✝ : Type ?u.46697
inst✝³ : Vec R Z✝
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.46721
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.46733
inst✝ : SemiInnerProductSpace R Z
T V : X → R
hT : HasAdjDiff R T
hV : HasAdjDiff R V
⊢ (fun Δt qₙ =>
      let ydg := <∂ (q:=qₙ), V q;
      fun pₙ =>
      let zdf := <∂ (q5:=ydg.1), (T pₙ + q5);
      let dy := zdf.2 1;
      let p' := pₙ - Δt • ydg.2 dy;
      let ydg := <∂ (p:=p'), T p;
      let zdf := <∂ (p4:=ydg.1), (p4 + V qₙ);
      let dy := zdf.2 1;
      let q' := qₙ + Δt • ydg.2 dy;
      (q', p')) =
    fun Δt qₙ =>
    let ydg := <∂ (q:=qₙ), V q;
    fun pₙ =>
    let ydg_1 :=
      <∂
        (p:=Function.invFun
          (fun x =>
            let zdf := <∂ (q5:=ydg.1), (T x + q5);
            let dy := zdf.2 1;
            x - (pₙ - Δt • ydg.2 dy))
          0),
        T p;
    let zdf := <∂ (p4:=ydg_1.1), (p4 + V qₙ);
    let dy := zdf.2 1;
    let q' := Function.invFun (fun x => x - (qₙ + Δt • ydg_1.2 dy)) 0;
    let p' :=
      Function.invFun
        (fun x =>
          let zdf := <∂ (q5:=ydg.1), (T x + q5);
          let dy := zdf.2 1;
          x - (pₙ - Δt • ydg.2 dy))
        0;
    (q', p')
Theorem: SciLean.explicitSymplecticEuler_eq_implicitSymplecticEulerV1
Proof state before:
R : Type u_1
inst✝⁶ : RCLike R
X✝ : Type ?u.46671
inst✝⁵ : Vec R X✝
Y✝ : Type ?u.46685
inst✝⁴ : Vec R Y✝
Z✝ : Type ?u.46697
inst✝³ : Vec R Z✝
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.46721
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.46733
inst✝ : SemiInnerProductSpace R Z
T V : X → R
hT : HasAdjDiff R T
hV : HasAdjDiff R V
⊢ (fun Δt qₙ =>
      let ydg := <∂ (q:=qₙ), V q;
      fun pₙ =>
      let zdf := <∂ (q5:=ydg.1), (T pₙ + q5);
      let dy := zdf.2 1;
      let p' := pₙ - Δt • ydg.2 dy;
      let ydg := <∂ (p:=p'), T p;
      let zdf := <∂ (p4:=ydg.1), (p4 + V qₙ);
      let dy := zdf.2 1;
      let q' := qₙ + Δt • ydg.2 dy;
      (q', p')) =
    fun Δt qₙ =>
    let ydg := <∂ (q:=qₙ), V q;
    fun pₙ =>
    let ydg_1 :=
      <∂
        (p:=Function.invFun
          (fun x =>
            let zdf := <∂ (q5:=ydg.1), (T x + q5);
            let dy := zdf.2 1;
            x - (pₙ - Δt • ydg.2 dy))
          0),
        T p;
    let zdf := <∂ (p4:=ydg_1.1), (p4 + V qₙ);
    let dy := zdf.2 1;
    let q' := Function.invFun (fun x => x - (qₙ + Δt • ydg_1.2 dy)) 0;
    let p' :=
      Function.invFun
        (fun x =>
          let zdf := <∂ (q5:=ydg.1), (T x + q5);
          let dy := zdf.2 1;
          x - (pₙ - Δt • ydg.2 dy))
        0;
    (q', p')
Tactic:
autodiff
Proof state after:
R : Type u_1
inst✝⁶ : RCLike R
X✝ : Type ?u.46671
inst✝⁵ : Vec R X✝
Y✝ : Type ?u.46685
inst✝⁴ : Vec R Y✝
Z✝ : Type ?u.46697
inst✝³ : Vec R Z✝
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.46721
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.46733
inst✝ : SemiInnerProductSpace R Z
T V : X → R
hT : HasAdjDiff R T
hV : HasAdjDiff R V
⊢ (fun Δt qₙ =>
      let ydg := <∂ (q:=qₙ), V q;
      fun pₙ =>
      let zdf := <∂ (q5:=ydg.1), (T pₙ + q5);
      let dy := zdf.2 1;
      let p' := pₙ - Δt • ydg.2 dy;
      let ydg := <∂ (p:=p'), T p;
      let zdf := <∂ (p4:=ydg.1), (p4 + V qₙ);
      let dy := zdf.2 1;
      let q' := qₙ + Δt • ydg.2 dy;
      (q', p')) =
    fun Δt qₙ =>
    let ydg := <∂ (q:=qₙ), V q;
    fun pₙ =>
    let ydg_1 :=
      <∂
        (p:=Function.invFun
          (fun x =>
            let zdf := <∂ (q5:=ydg.1), (T x + q5);
            let dy := zdf.2 1;
            x - (pₙ - Δt • ydg.2 dy))
          0),
        T p;
    let zdf := <∂ (p4:=ydg_1.1), (p4 + V qₙ);
    let dy := zdf.2 1;
    let q' := qₙ + Δt • ydg_1.2 dy;
    let p' :=
      Function.invFun
        (fun x =>
          let zdf := <∂ (q5:=ydg.1), (T x + q5);
          let dy := zdf.2 1;
          x - (pₙ - Δt • ydg.2 dy))
        0;
    (q', p')
Theorem: SciLean.explicitSymplecticEuler_eq_implicitSymplecticEulerV1
Proof state before:
R : Type u_1
inst✝⁶ : RCLike R
X✝ : Type ?u.46671
inst✝⁵ : Vec R X✝
Y✝ : Type ?u.46685
inst✝⁴ : Vec R Y✝
Z✝ : Type ?u.46697
inst✝³ : Vec R Z✝
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.46721
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.46733
inst✝ : SemiInnerProductSpace R Z
T V : X → R
hT : HasAdjDiff R T
hV : HasAdjDiff R V
⊢ (fun Δt qₙ =>
      let ydg := <∂ (q:=qₙ), V q;
      fun pₙ =>
      let zdf := <∂ (q5:=ydg.1), (T pₙ + q5);
      let dy := zdf.2 1;
      let p' := pₙ - Δt • ydg.2 dy;
      let ydg := <∂ (p:=p'), T p;
      let zdf := <∂ (p4:=ydg.1), (p4 + V qₙ);
      let dy := zdf.2 1;
      let q' := qₙ + Δt • ydg.2 dy;
      (q', p')) =
    fun Δt qₙ =>
    let ydg := <∂ (q:=qₙ), V q;
    fun pₙ =>
    let ydg_1 :=
      <∂
        (p:=Function.invFun
          (fun x =>
            let zdf := <∂ (q5:=ydg.1), (T x + q5);
            let dy := zdf.2 1;
            x - (pₙ - Δt • ydg.2 dy))
          0),
        T p;
    let zdf := <∂ (p4:=ydg_1.1), (p4 + V qₙ);
    let dy := zdf.2 1;
    let q' := qₙ + Δt • ydg_1.2 dy;
    let p' :=
      Function.invFun
        (fun x =>
          let zdf := <∂ (q5:=ydg.1), (T x + q5);
          let dy := zdf.2 1;
          x - (pₙ - Δt • ydg.2 dy))
        0;
    (q', p')
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: pair_add
Proof state before:
X : Type u_1
Y : Type u_2
inst✝¹ : Add X
inst✝ : Add Y
x x' : X
y y' : Y
⊢ (x, y) + (x', y') = (x + x', y + y')
Tactic:
simp[HAdd.hAdd, Add.add]
Proof state after:
no goals
Theorem: SciLean.val_erase
Proof state before:
α : Sort u_1
a : α
⊢ RunTimeErased.val (erase a) = a
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.approx_consistency
Proof state before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Nonempty α
N : Type
lN : Filter N
inst✝ : T2Space α
spec : α → Prop
approx : ApproxSolution lN spec
⊢ ∀ (a : α), (a = limit n ∈ lN, ApproxSolution.val approx n) → spec a
Tactic:
induction approx
Proof state after:
case exact
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Nonempty α
N : Type
lN : Filter N
inst✝ : T2Space α
spec spec✝ : α → Prop
impl✝ : α
h✝ : spec✝ impl✝
⊢ ∀ (a : α), (a = limit n ∈ ⊤, ApproxSolution.val (ApproxSolution.exact impl✝ h✝) n) → spec✝ a

case approx
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Nonempty α
N : Type
lN : Filter N
inst✝ : T2Space α
spec : α → Prop
N✝ M✝ : Type
spec✝ : α → Prop
specₙ✝ : N✝ → α → Prop
lN✝ : Filter N✝
lM✝ : Filter M✝
consistent✝ : ∀ (aₙ : N✝ → α), (∀ (n : N✝), specₙ✝ n (aₙ n)) → ∀ (a : α), (a = limit n ∈ lN✝, aₙ n) → spec✝ a
convergence✝ :
  ∀ (a' : N✝ → M✝ → α),
    (∀ (n : N✝), specₙ✝ n (limit m ∈ lM✝, a' n m)) →
      ∃ a,
        a =
          limit x ∈ Filter.prod lN✝ lM✝,
            match x with
            | (n, m) => a' n m
impl✝ : (n : N✝) → ApproxSolution lM✝ (specₙ✝ n)
impl_ih✝ : ∀ (n : N✝) (a : α), (a = limit n_1 ∈ lM✝, ApproxSolution.val (impl✝ n) n_1) → specₙ✝ n a
⊢ ∀ (a : α),
    (a =
        limit n ∈ Filter.prod lN✝ lM✝,
          ApproxSolution.val (ApproxSolution.approx specₙ✝ lN✝ lM✝ consistent✝ convergence✝ impl✝) n) →
      spec✝ a
Theorem: SciLean.approx_consistency
Proof state before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Nonempty α
N : Type
lN : Filter N
inst✝ : T2Space α
spec spec✝ : α → Prop
impl : α
h : spec✝ impl
⊢ ∀ (a : α), (a = limit n ∈ ⊤, ApproxSolution.val (ApproxSolution.exact impl h) n) → spec✝ a
Tactic:
case exact impl h =>
  simp[ApproxSolution.val]
  sorry_proof
Proof state after:
no goals
Theorem: SciLean.approx_consistency
Proof state before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Nonempty α
N : Type
lN✝ : Filter N
inst✝ : T2Space α
spec : α → Prop
N✝ M✝ : Type
spec✝ : α → Prop
specₙ : N✝ → α → Prop
lN : Filter N✝
lM : Filter M✝
consistent : ∀ (aₙ : N✝ → α), (∀ (n : N✝), specₙ n (aₙ n)) → ∀ (a : α), (a = limit n ∈ lN, aₙ n) → spec✝ a
convergence :
  ∀ (a' : N✝ → M✝ → α),
    (∀ (n : N✝), specₙ n (limit m ∈ lM, a' n m)) →
      ∃ a,
        a =
          limit x ∈ Filter.prod lN lM,
            match x with
            | (n, m) => a' n m
impl : (n : N✝) → ApproxSolution lM (specₙ n)
hn : ∀ (n : N✝) (a : α), (a = limit n_1 ∈ lM, ApproxSolution.val (impl n) n_1) → specₙ n a
⊢ ∀ (a : α),
    (a =
        limit n ∈ Filter.prod lN lM,
          ApproxSolution.val (ApproxSolution.approx specₙ lN lM consistent convergence impl) n) →
      spec✝ a
Tactic:
case approx specₙ lN lM consistent convergence impl hn =>
  simp[ApproxSolution.val]
  let aₙ := λ n => lim (lM.map λ m => (impl n).val m)
  sorry_proof
Proof state after:
no goals
Theorem: SciLean.approx_consistency
Proof state before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Nonempty α
N : Type
lN : Filter N
inst✝ : T2Space α
spec spec✝ : α → Prop
impl : α
h : spec✝ impl
⊢ ∀ (a : α), (a = limit n ∈ ⊤, ApproxSolution.val (ApproxSolution.exact impl h) n) → spec✝ a
Tactic:
simp[ApproxSolution.val]
Proof state after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Nonempty α
N : Type
lN : Filter N
inst✝ : T2Space α
spec spec✝ : α → Prop
impl : α
h : spec✝ impl
⊢ spec✝ impl
Theorem: SciLean.approx_consistency
Proof state before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Nonempty α
N : Type
lN : Filter N
inst✝ : T2Space α
spec spec✝ : α → Prop
impl : α
h : spec✝ impl
⊢ spec✝ impl
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.approx_consistency
Proof state before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Nonempty α
N : Type
lN✝ : Filter N
inst✝ : T2Space α
spec : α → Prop
N✝ M✝ : Type
spec✝ : α → Prop
specₙ : N✝ → α → Prop
lN : Filter N✝
lM : Filter M✝
consistent : ∀ (aₙ : N✝ → α), (∀ (n : N✝), specₙ n (aₙ n)) → ∀ (a : α), (a = limit n ∈ lN, aₙ n) → spec✝ a
convergence :
  ∀ (a' : N✝ → M✝ → α),
    (∀ (n : N✝), specₙ n (limit m ∈ lM, a' n m)) →
      ∃ a,
        a =
          limit x ∈ Filter.prod lN lM,
            match x with
            | (n, m) => a' n m
impl : (n : N✝) → ApproxSolution lM (specₙ n)
hn : ∀ (n : N✝) (a : α), (a = limit n_1 ∈ lM, ApproxSolution.val (impl n) n_1) → specₙ n a
⊢ ∀ (a : α),
    (a =
        limit n ∈ Filter.prod lN lM,
          ApproxSolution.val (ApproxSolution.approx specₙ lN lM consistent convergence impl) n) →
      spec✝ a
Tactic:
simp[ApproxSolution.val]
Proof state after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Nonempty α
N : Type
lN✝ : Filter N
inst✝ : T2Space α
spec : α → Prop
N✝ M✝ : Type
spec✝ : α → Prop
specₙ : N✝ → α → Prop
lN : Filter N✝
lM : Filter M✝
consistent : ∀ (aₙ : N✝ → α), (∀ (n : N✝), specₙ n (aₙ n)) → ∀ (a : α), (a = limit n ∈ lN, aₙ n) → spec✝ a
convergence :
  ∀ (a' : N✝ → M✝ → α),
    (∀ (n : N✝), specₙ n (limit m ∈ lM, a' n m)) →
      ∃ a,
        a =
          limit x ∈ Filter.prod lN lM,
            match x with
            | (n, m) => a' n m
impl : (n : N✝) → ApproxSolution lM (specₙ n)
hn : ∀ (n : N✝) (a : α), (a = limit n_1 ∈ lM, ApproxSolution.val (impl n) n_1) → specₙ n a
⊢ spec✝ (limit n ∈ Filter.prod lN lM, ApproxSolution.val (impl n.1) n.2)
Theorem: SciLean.approx_consistency
Proof state before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Nonempty α
N : Type
lN✝ : Filter N
inst✝ : T2Space α
spec : α → Prop
N✝ M✝ : Type
spec✝ : α → Prop
specₙ : N✝ → α → Prop
lN : Filter N✝
lM : Filter M✝
consistent : ∀ (aₙ : N✝ → α), (∀ (n : N✝), specₙ n (aₙ n)) → ∀ (a : α), (a = limit n ∈ lN, aₙ n) → spec✝ a
convergence :
  ∀ (a' : N✝ → M✝ → α),
    (∀ (n : N✝), specₙ n (limit m ∈ lM, a' n m)) →
      ∃ a,
        a =
          limit x ∈ Filter.prod lN lM,
            match x with
            | (n, m) => a' n m
impl : (n : N✝) → ApproxSolution lM (specₙ n)
hn : ∀ (n : N✝) (a : α), (a = limit n_1 ∈ lM, ApproxSolution.val (impl n) n_1) → specₙ n a
⊢ spec✝ (limit n ∈ Filter.prod lN lM, ApproxSolution.val (impl n.1) n.2)
Tactic:
let aₙ := λ n => lim (lM.map λ m => (impl n).val m)
Proof state after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Nonempty α
N : Type
lN✝ : Filter N
inst✝ : T2Space α
spec : α → Prop
N✝ M✝ : Type
spec✝ : α → Prop
specₙ : N✝ → α → Prop
lN : Filter N✝
lM : Filter M✝
consistent : ∀ (aₙ : N✝ → α), (∀ (n : N✝), specₙ n (aₙ n)) → ∀ (a : α), (a = limit n ∈ lN, aₙ n) → spec✝ a
convergence :
  ∀ (a' : N✝ → M✝ → α),
    (∀ (n : N✝), specₙ n (limit m ∈ lM, a' n m)) →
      ∃ a,
        a =
          limit x ∈ Filter.prod lN lM,
            match x with
            | (n, m) => a' n m
impl : (n : N✝) → ApproxSolution lM (specₙ n)
hn : ∀ (n : N✝) (a : α), (a = limit n_1 ∈ lM, ApproxSolution.val (impl n) n_1) → specₙ n a
aₙ : N✝ → α := fun n => lim (Filter.map (fun m => ApproxSolution.val (impl n) m) lM)
⊢ spec✝ (limit n ∈ Filter.prod lN lM, ApproxSolution.val (impl n.1) n.2)
Theorem: SciLean.approx_consistency
Proof state before:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Nonempty α
N : Type
lN✝ : Filter N
inst✝ : T2Space α
spec : α → Prop
N✝ M✝ : Type
spec✝ : α → Prop
specₙ : N✝ → α → Prop
lN : Filter N✝
lM : Filter M✝
consistent : ∀ (aₙ : N✝ → α), (∀ (n : N✝), specₙ n (aₙ n)) → ∀ (a : α), (a = limit n ∈ lN, aₙ n) → spec✝ a
convergence :
  ∀ (a' : N✝ → M✝ → α),
    (∀ (n : N✝), specₙ n (limit m ∈ lM, a' n m)) →
      ∃ a,
        a =
          limit x ∈ Filter.prod lN lM,
            match x with
            | (n, m) => a' n m
impl : (n : N✝) → ApproxSolution lM (specₙ n)
hn : ∀ (n : N✝) (a : α), (a = limit n_1 ∈ lM, ApproxSolution.val (impl n) n_1) → specₙ n a
aₙ : N✝ → α := fun n => lim (Filter.map (fun m => ApproxSolution.val (impl n) m) lM)
⊢ spec✝ (limit n ∈ Filter.prod lN lM, ApproxSolution.val (impl n.1) n.2)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Rand.harmonicRec.arg_x.CDifferentiable_rule
Proof state before:
Y : Type
inst✝³ : SemiHilbert Float Y
inst✝² : Module ℝ Y
inst✝¹ : IsScalarTower ℝ Float Y
inst✝ : MeasurableSpace Y
n : ℕ
φ : Vec3 → Float
g : Vec3 → Y
hφ : CDifferentiable Float φ
hg : CDifferentiable Float g
⊢ CDifferentiable Float fun x => harmonicRec n φ g x
Tactic:
induction n <;> (simp[harmonicRec]; fun_prop)
Proof state after:
no goals
Theorem: SciLean.Rand.harmonicRec.arg_x.CDifferentiable_rule
Proof state before:
case succ
Y : Type
inst✝³ : SemiHilbert Float Y
inst✝² : Module ℝ Y
inst✝¹ : IsScalarTower ℝ Float Y
inst✝ : MeasurableSpace Y
φ : Vec3 → Float
g : Vec3 → Y
hφ : CDifferentiable Float φ
hg : CDifferentiable Float g
n✝ : ℕ
n_ih✝ : CDifferentiable Float fun x => harmonicRec n✝ φ g x
⊢ CDifferentiable Float fun x => harmonicRec (Nat.succ n✝) φ g x
Tactic:
simp[harmonicRec]
Proof state after:
case succ
Y : Type
inst✝³ : SemiHilbert Float Y
inst✝² : Module ℝ Y
inst✝¹ : IsScalarTower ℝ Float Y
inst✝ : MeasurableSpace Y
φ : Vec3 → Float
g : Vec3 → Y
hφ : CDifferentiable Float φ
hg : CDifferentiable Float g
n✝ : ℕ
n_ih✝ : CDifferentiable Float fun x => harmonicRec n✝ φ g x
⊢ CDifferentiable Float fun x => (pi'⁻¹ * 4⁻¹) • ∫' x', harmonicRec n✝ φ g (x + φ x • ↑x')
Theorem: SciLean.Rand.harmonicRec.arg_x.CDifferentiable_rule
Proof state before:
case succ
Y : Type
inst✝³ : SemiHilbert Float Y
inst✝² : Module ℝ Y
inst✝¹ : IsScalarTower ℝ Float Y
inst✝ : MeasurableSpace Y
φ : Vec3 → Float
g : Vec3 → Y
hφ : CDifferentiable Float φ
hg : CDifferentiable Float g
n✝ : ℕ
n_ih✝ : CDifferentiable Float fun x => harmonicRec n✝ φ g x
⊢ CDifferentiable Float fun x => (pi'⁻¹ * 4⁻¹) • ∫' x', harmonicRec n✝ φ g (x + φ x • ↑x')
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.Rand.harmonicRec'_CDifferentiable
Proof state before:
Y : Type
inst✝³ : SemiHilbert Float Y
inst✝² : Module ℝ Y
inst✝¹ : IsScalarTower ℝ Float Y
inst✝ : MeasurableSpace Y
n : ℕ
⊢ CDifferentiable Float fun w => harmonicRec' n w.1 w.2.1 w.2.2
Tactic:
induction n <;> (simp[harmonicRec']; fun_prop)
Proof state after:
no goals
Theorem: SciLean.Rand.harmonicRec'_CDifferentiable
Proof state before:
case succ
Y : Type
inst✝³ : SemiHilbert Float Y
inst✝² : Module ℝ Y
inst✝¹ : IsScalarTower ℝ Float Y
inst✝ : MeasurableSpace Y
n✝ : ℕ
n_ih✝ : CDifferentiable Float fun w => harmonicRec' n✝ w.1 w.2.1 w.2.2
⊢ CDifferentiable Float fun w => harmonicRec' (Nat.succ n✝) w.1 w.2.1 w.2.2
Tactic:
simp[harmonicRec']
Proof state after:
case succ
Y : Type
inst✝³ : SemiHilbert Float Y
inst✝² : Module ℝ Y
inst✝¹ : IsScalarTower ℝ Float Y
inst✝ : MeasurableSpace Y
n✝ : ℕ
n_ih✝ : CDifferentiable Float fun w => harmonicRec' n✝ w.1 w.2.1 w.2.2
⊢ CDifferentiable Float fun w => (pi'⁻¹ * 4⁻¹) • ∫' x', harmonicRec' n✝ w.1 w.2.1 (w.2.2 + w.1 w.2.2 • ↑x')
Theorem: SciLean.Rand.harmonicRec'_CDifferentiable
Proof state before:
case succ
Y : Type
inst✝³ : SemiHilbert Float Y
inst✝² : Module ℝ Y
inst✝¹ : IsScalarTower ℝ Float Y
inst✝ : MeasurableSpace Y
n✝ : ℕ
n_ih✝ : CDifferentiable Float fun w => harmonicRec' n✝ w.1 w.2.1 w.2.2
⊢ CDifferentiable Float fun w => (pi'⁻¹ * 4⁻¹) • ∫' x', harmonicRec' n✝ w.1 w.2.1 (w.2.2 + w.1 w.2.2 • ↑x')
Tactic:
fun_prop
Proof state after:
no goals
Theorem: Function.invFun.id_rule
Proof state before:
X : Type u_1
inst✝⁴ : Nonempty X
Y : Type ?u.53
inst✝³ : Nonempty Y
Z : Type ?u.59
inst✝² : Nonempty Z
X₁ : Type ?u.65
inst✝¹ : Nonempty X₁
X₂ : Type ?u.71
inst✝ : Nonempty X₂
⊢ (invFun fun x => x) = fun x => x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.invFun.comp_rule
Proof state before:
X : Type u_3
inst✝⁴ : Nonempty X
Y : Type u_1
inst✝³ : Nonempty Y
Z : Type u_2
inst✝² : Nonempty Z
X₁ : Type ?u.169
inst✝¹ : Nonempty X₁
X₂ : Type ?u.175
inst✝ : Nonempty X₂
f : Y → Z
g : X → Y
hf : Bijective f
hg : Bijective g
⊢ (invFun fun x => f (g x)) = fun z =>
    let y := invFun f z;
    let x := invFun g y;
    x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.invFun.let_rule
Proof state before:
X : Type u_5
inst✝⁴ : Nonempty X
Y : Type u_1
inst✝³ : Nonempty Y
Z : Type u_3
inst✝² : Nonempty Z
X₁ : Type u_4
inst✝¹ : Nonempty X₁
X₂ : Type u_2
inst✝ : Nonempty X₂
f : X₂ → Y → Z
g : X₁ → Y
p₁ : X → X₁
p₂ : X → X₂
hf : Bijective fun xy => f xy.1 xy.2
hg : Bijective g
hp : Bijective fun x => (p₁ x, p₂ x)
⊢ (invFun fun x =>
      let y := g (p₁ x);
      f (p₂ x) y) =
    fun z =>
    let x₂y := invFun (fun xy => f xy.1 xy.2) z;
    let x₁ := invFun g x₂y.2;
    let x := invFun (fun x => (p₁ x, p₂ x)) (x₁, x₂y.1);
    x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.invFun.Prod.mk.arg_fstsnd.invFun_rule
Proof state before:
X✝ : Type ?u.713
inst✝⁷ : Nonempty X✝
Y✝ : Type ?u.719
inst✝⁶ : Nonempty Y✝
Z✝ : Type ?u.725
inst✝⁵ : Nonempty Z✝
X₁ : Type u_1
inst✝⁴ : Nonempty X₁
X₂ : Type u_3
inst✝³ : Nonempty X₂
X : Type u_5
inst✝² : Nonempty X
Y : Type u_2
inst✝¹ : Nonempty Y
Z : Type u_4
inst✝ : Nonempty Z
f : X₁ → Y
g : X₂ → Z
p₁ : X → X₁
p₂ : X → X₂
hf : Bijective f
hg : Bijective g
hp : Bijective fun x => (p₁ x, p₂ x)
⊢ (invFun fun x => (f (p₁ x), g (p₂ x))) = fun yz =>
    let x₁ := invFun f yz.1;
    let x₂ := invFun g yz.2;
    let x := invFun (fun x => (p₁ x, p₂ x)) (x₁, x₂);
    x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.invFun.Neg.neg.arg_a0.invFun_rule
Proof state before:
X✝ : Type ?u.1107
inst✝⁸ : Nonempty X✝
Y✝ : Type ?u.1113
inst✝⁷ : Nonempty Y✝
Z✝ : Type ?u.1119
inst✝⁶ : Nonempty Z✝
X₁ : Type ?u.1125
inst✝⁵ : Nonempty X₁
X₂ : Type ?u.1131
inst✝⁴ : Nonempty X₂
X : Type u_2
inst✝³ : Nonempty X
Y : Type u_1
inst✝² : Nonempty Y
Z : Type ?u.1149
inst✝¹ : Nonempty Z
inst✝ : AddGroup Y
f : X → Y
hf : Bijective f
⊢ (invFun fun x => -f x) = fun y => invFun f (-y)
Tactic:
sorry_proof
Proof state after:
no goals