internlm/Lean-Github huggingface dataset:
Theorem: SciLean.SciLean.semiAdjoint.arg_y.CDifferentiable_rule
Proof state before:
K✝ : Type ?u.91910
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.91916
inst✝¹⁶ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.91929
inst✝¹⁵ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.91940
inst✝¹⁴ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.91951
inst✝¹³ : IndexType ι✝
inst✝¹² : LawfulIndexType ι✝
inst✝¹¹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.91978
inst✝¹⁰ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_2
inst✝⁹ : RCLike K
X : Type u_3
inst✝⁸ : SemiInnerProductSpace K X
Y : Type u_4
inst✝⁷ : SemiInnerProductSpace K Y
Z : Type ?u.92024
inst✝⁶ : SemiInnerProductSpace K Z
W✝ : Type ?u.92035
inst✝⁵ : SemiInnerProductSpace K W✝
ι : Type ?u.92046
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
E : ι → Type ?u.92073
inst✝¹ : (i : ι) → SemiInnerProductSpace K (E i)
W : Type u_1
inst✝ : Vec K W
f : X → Y
a0 : W → Y
hf : CDifferentiable K f
ha0 : CDifferentiable K a0
⊢ CDifferentiable K fun w => semiAdjoint K f (a0 w)
Tactic:
intro x
Proof state after:
K✝ : Type ?u.91910
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.91916
inst✝¹⁶ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.91929
inst✝¹⁵ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.91940
inst✝¹⁴ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.91951
inst✝¹³ : IndexType ι✝
inst✝¹² : LawfulIndexType ι✝
inst✝¹¹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.91978
inst✝¹⁰ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_2
inst✝⁹ : RCLike K
X : Type u_3
inst✝⁸ : SemiInnerProductSpace K X
Y : Type u_4
inst✝⁷ : SemiInnerProductSpace K Y
Z : Type ?u.92024
inst✝⁶ : SemiInnerProductSpace K Z
W✝ : Type ?u.92035
inst✝⁵ : SemiInnerProductSpace K W✝
ι : Type ?u.92046
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
E : ι → Type ?u.92073
inst✝¹ : (i : ι) → SemiInnerProductSpace K (E i)
W : Type u_1
inst✝ : Vec K W
f : X → Y
a0 : W → Y
hf : CDifferentiable K f
ha0 : CDifferentiable K a0
x : W
⊢ CDifferentiableAt K (fun w => semiAdjoint K f (a0 w)) x
Theorem: SciLean.SciLean.semiAdjoint.arg_y.CDifferentiable_rule
Proof state before:
K✝ : Type ?u.91910
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.91916
inst✝¹⁶ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.91929
inst✝¹⁵ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.91940
inst✝¹⁴ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.91951
inst✝¹³ : IndexType ι✝
inst✝¹² : LawfulIndexType ι✝
inst✝¹¹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.91978
inst✝¹⁰ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_2
inst✝⁹ : RCLike K
X : Type u_3
inst✝⁸ : SemiInnerProductSpace K X
Y : Type u_4
inst✝⁷ : SemiInnerProductSpace K Y
Z : Type ?u.92024
inst✝⁶ : SemiInnerProductSpace K Z
W✝ : Type ?u.92035
inst✝⁵ : SemiInnerProductSpace K W✝
ι : Type ?u.92046
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
E : ι → Type ?u.92073
inst✝¹ : (i : ι) → SemiInnerProductSpace K (E i)
W : Type u_1
inst✝ : Vec K W
f : X → Y
a0 : W → Y
hf : CDifferentiable K f
ha0 : CDifferentiable K a0
x : W
⊢ CDifferentiableAt K (fun w => semiAdjoint K f (a0 w)) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.SciLean.semiAdjoint.arg_y.HasAdjDiffAt_rule
Proof state before:
K✝ : Type ?u.92576
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.92582
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.92595
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.92606
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.92617
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.92644
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.92690
inst✝⁵ : SemiInnerProductSpace K Z
W : Type u_4
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.92712
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.92739
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
w : W
f : X → Y
a0 : W → Y
hf : CDifferentiable K f
ha0 : HasAdjDiffAt K a0 w
⊢ HasAdjDiffAt K (fun w => semiAdjoint K f (a0 w)) w
Tactic:
constructor
Proof state after:
case left
K✝ : Type ?u.92576
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.92582
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.92595
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.92606
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.92617
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.92644
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.92690
inst✝⁵ : SemiInnerProductSpace K Z
W : Type u_4
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.92712
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.92739
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
w : W
f : X → Y
a0 : W → Y
hf : CDifferentiable K f
ha0 : HasAdjDiffAt K a0 w
⊢ CDifferentiableAt K (fun w => semiAdjoint K f (a0 w)) w

case right
K✝ : Type ?u.92576
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.92582
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.92595
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.92606
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.92617
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.92644
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.92690
inst✝⁵ : SemiInnerProductSpace K Z
W : Type u_4
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.92712
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.92739
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
w : W
f : X → Y
a0 : W → Y
hf : CDifferentiable K f
ha0 : HasAdjDiffAt K a0 w
⊢ HasSemiAdjoint K (cderiv K (fun w => semiAdjoint K f (a0 w)) w)
Theorem: SciLean.SciLean.semiAdjoint.arg_y.HasAdjDiffAt_rule
Proof state before:
case left
K✝ : Type ?u.92576
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.92582
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.92595
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.92606
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.92617
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.92644
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.92690
inst✝⁵ : SemiInnerProductSpace K Z
W : Type u_4
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.92712
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.92739
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
w : W
f : X → Y
a0 : W → Y
hf : CDifferentiable K f
ha0 : HasAdjDiffAt K a0 w
⊢ CDifferentiableAt K (fun w => semiAdjoint K f (a0 w)) w

case right
K✝ : Type ?u.92576
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.92582
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.92595
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.92606
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.92617
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.92644
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.92690
inst✝⁵ : SemiInnerProductSpace K Z
W : Type u_4
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.92712
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.92739
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
w : W
f : X → Y
a0 : W → Y
hf : CDifferentiable K f
ha0 : HasAdjDiffAt K a0 w
⊢ HasSemiAdjoint K (cderiv K (fun w => semiAdjoint K f (a0 w)) w)
Tactic:
fun_prop
Proof state after:
case right
K✝ : Type ?u.92576
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.92582
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.92595
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.92606
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.92617
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.92644
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.92690
inst✝⁵ : SemiInnerProductSpace K Z
W : Type u_4
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.92712
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.92739
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
w : W
f : X → Y
a0 : W → Y
hf : CDifferentiable K f
ha0 : HasAdjDiffAt K a0 w
⊢ HasSemiAdjoint K (cderiv K (fun w => semiAdjoint K f (a0 w)) w)
Theorem: SciLean.SciLean.semiAdjoint.arg_y.HasAdjDiffAt_rule
Proof state before:
case right
K✝ : Type ?u.92576
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.92582
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.92595
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.92606
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.92617
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.92644
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.92690
inst✝⁵ : SemiInnerProductSpace K Z
W : Type u_4
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.92712
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.92739
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
w : W
f : X → Y
a0 : W → Y
hf : CDifferentiable K f
ha0 : HasAdjDiffAt K a0 w
⊢ HasSemiAdjoint K (cderiv K (fun w => semiAdjoint K f (a0 w)) w)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.SciLean.semiAdjoint.arg_y.HasAdjDiff_rule
Proof state before:
K✝ : Type ?u.93469
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.93475
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.93488
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.93499
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.93510
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.93537
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.93583
inst✝⁵ : SemiInnerProductSpace K Z
W : Type u_4
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.93605
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.93632
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y
a0 : W → Y
hf : CDifferentiable K f
ha0 : HasAdjDiff K a0
⊢ HasAdjDiff K fun w => semiAdjoint K f (a0 w)
Tactic:
intro w
Proof state after:
K✝ : Type ?u.93469
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.93475
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.93488
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.93499
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.93510
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.93537
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.93583
inst✝⁵ : SemiInnerProductSpace K Z
W : Type u_4
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.93605
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.93632
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y
a0 : W → Y
hf : CDifferentiable K f
ha0 : HasAdjDiff K a0
w : W
⊢ HasAdjDiffAt K (fun w => semiAdjoint K f (a0 w)) w
Theorem: SciLean.SciLean.semiAdjoint.arg_y.HasAdjDiff_rule
Proof state before:
K✝ : Type ?u.93469
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.93475
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.93488
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.93499
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.93510
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.93537
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.93583
inst✝⁵ : SemiInnerProductSpace K Z
W : Type u_4
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.93605
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.93632
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y
a0 : W → Y
hf : CDifferentiable K f
ha0 : HasAdjDiff K a0
w : W
⊢ HasAdjDiffAt K (fun w => semiAdjoint K f (a0 w)) w
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.parametric_inverse_affine
Proof state before:
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ : X → R
n : ℕ
f : X → R
c : R
hf : IsAffineMap R f
hn : autoParam (n + 1 = card ι) _auto✝
⊢ let u := ∇ f 0;
  let dec := planeDecomposition u hn;
  ParametricInverseAt f c (fun x y t => dec (t, y)) (fun x x => (c - f 0) / ‖u‖₂[R]) fun x => ⊤
Tactic:
simp[ParametricInverseAt,arrayTypeCont]
Proof state after:
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ : X → R
n : ℕ
f : X → R
c : R
hf : IsAffineMap R f
hn : autoParam (n + 1 = card ι) _auto✝
⊢ ∀ (x₁ : DataArrayN R (Fin n)), f ((planeDecomposition (∇ f 0) hn) ((c - f 0) / ‖∇ f 0‖₂[R], x₁)) = c
Theorem: SciLean.parametric_inverse_affine
Proof state before:
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ : X → R
n : ℕ
f : X → R
c : R
hf : IsAffineMap R f
hn : autoParam (n + 1 = card ι) _auto✝
⊢ ∀ (x₁ : DataArrayN R (Fin n)), f ((planeDecomposition (∇ f 0) hn) ((c - f 0) / ‖∇ f 0‖₂[R], x₁)) = c
Tactic:
have h : f = fun x => ⟪(∇ f 0), x⟫ + f 0 := sorry_proof
Proof state after:
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ : X → R
n : ℕ
f : X → R
c : R
hf : IsAffineMap R f
hn : autoParam (n + 1 = card ι) _auto✝
h : f = fun x => ⟪∇ f 0, x⟫_R + f 0
⊢ ∀ (x₁ : DataArrayN R (Fin n)), f ((planeDecomposition (∇ f 0) hn) ((c - f 0) / ‖∇ f 0‖₂[R], x₁)) = c
Theorem: SciLean.parametric_inverse_affine
Proof state before:
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ : X → R
n : ℕ
f : X → R
c : R
hf : IsAffineMap R f
hn : autoParam (n + 1 = card ι) _auto✝
h : f = fun x => ⟪∇ f 0, x⟫_R + f 0
⊢ ∀ (x₁ : DataArrayN R (Fin n)), f ((planeDecomposition (∇ f 0) hn) ((c - f 0) / ‖∇ f 0‖₂[R], x₁)) = c
Tactic:
rw[h]
Proof state after:
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ : X → R
n : ℕ
f : X → R
c : R
hf : IsAffineMap R f
hn : autoParam (n + 1 = card ι) _auto✝
h : f = fun x => ⟪∇ f 0, x⟫_R + f 0
⊢ ∀ (x₁ : DataArrayN R (Fin n)),
    (fun x => ⟪∇ f 0, x⟫_R + f 0)
        ((planeDecomposition (∇ (x:=0), (⟪∇ f 0, x⟫_R + f 0)) hn)
          ((c - (fun x => ⟪∇ f 0, x⟫_R + f 0) 0) / ‖∇ (x:=0), (⟪∇ f 0, x⟫_R + f 0)‖₂[R], x₁)) =
      c
Theorem: SciLean.parametric_inverse_affine
Proof state before:
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ : X → R
n : ℕ
f : X → R
c : R
hf : IsAffineMap R f
hn : autoParam (n + 1 = card ι) _auto✝
h : f = fun x => ⟪∇ f 0, x⟫_R + f 0
⊢ ∀ (x₁ : DataArrayN R (Fin n)),
    (fun x => ⟪∇ f 0, x⟫_R + f 0)
        ((planeDecomposition (∇ (x:=0), (⟪∇ f 0, x⟫_R + f 0)) hn)
          ((c - (fun x => ⟪∇ f 0, x⟫_R + f 0) 0) / ‖∇ (x:=0), (⟪∇ f 0, x⟫_R + f 0)‖₂[R], x₁)) =
      c
Tactic:
fun_trans [scalarGradient,planeDecomposition_orthogonal_dir]
Proof state after:
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ : X → R
n : ℕ
f : X → R
c : R
hf : IsAffineMap R f
hn : autoParam (n + 1 = card ι) _auto✝
h : f = fun x => ⟪∇ f 0, x⟫_R + f 0
⊢ (c - f 0) / ‖(<∂ f 0).2 1‖₂[R] * ‖(<∂ f 0).2 1‖₂[R] + f 0 = c
Theorem: SciLean.parametric_inverse_affine
Proof state before:
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ : X → R
n : ℕ
f : X → R
c : R
hf : IsAffineMap R f
hn : autoParam (n + 1 = card ι) _auto✝
h : f = fun x => ⟪∇ f 0, x⟫_R + f 0
⊢ (c - f 0) / ‖(<∂ f 0).2 1‖₂[R] * ‖(<∂ f 0).2 1‖₂[R] + f 0 = c
Tactic:
have : ‖(<∂ f 0).2 1‖₂[R] ≠ 0 := sorry_proof
Proof state after:
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ : X → R
n : ℕ
f : X → R
c : R
hf : IsAffineMap R f
hn : autoParam (n + 1 = card ι) _auto✝
h : f = fun x => ⟪∇ f 0, x⟫_R + f 0
this : ‖(<∂ f 0).2 1‖₂[R] ≠ 0
⊢ (c - f 0) / ‖(<∂ f 0).2 1‖₂[R] * ‖(<∂ f 0).2 1‖₂[R] + f 0 = c
Theorem: SciLean.parametric_inverse_affine
Proof state before:
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ : X → R
n : ℕ
f : X → R
c : R
hf : IsAffineMap R f
hn : autoParam (n + 1 = card ι) _auto✝
h : f = fun x => ⟪∇ f 0, x⟫_R + f 0
this : ‖(<∂ f 0).2 1‖₂[R] ≠ 0
⊢ (c - f 0) / ‖(<∂ f 0).2 1‖₂[R] * ‖(<∂ f 0).2 1‖₂[R] + f 0 = c
Tactic:
field_simp
Proof state after:
no goals
Theorem: SciLean.parametric_inverse_affine'
Proof state before:
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ f : X → R
c : R
hf : IsAffineMap R f
⊢ let u := ∇ f 0;
  let dec := planeDecomposition u ⋯;
  ParametricInverseAt f c (fun x y t => dec (t, y)) (fun x x => (c - f 0) / ‖u‖₂[R]) fun x => ⊤
Tactic:
simp[ParametricInverseAt,arrayTypeCont]
Proof state after:
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ f : X → R
c : R
hf : IsAffineMap R f
⊢ ∀ (x₁ : DataArrayN R (Fin (card ι - 1))), f ((planeDecomposition (∇ f 0) ⋯) ((c - f 0) / ‖∇ f 0‖₂[R], x₁)) = c
Theorem: SciLean.parametric_inverse_affine'
Proof state before:
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ f : X → R
c : R
hf : IsAffineMap R f
⊢ ∀ (x₁ : DataArrayN R (Fin (card ι - 1))), f ((planeDecomposition (∇ f 0) ⋯) ((c - f 0) / ‖∇ f 0‖₂[R], x₁)) = c
Tactic:
have h : f = fun x => ⟪(∇ f 0), x⟫ + f 0 := sorry_proof
Proof state after:
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ f : X → R
c : R
hf : IsAffineMap R f
h : f = fun x => ⟪∇ f 0, x⟫_R + f 0
⊢ ∀ (x₁ : DataArrayN R (Fin (card ι - 1))), f ((planeDecomposition (∇ f 0) ⋯) ((c - f 0) / ‖∇ f 0‖₂[R], x₁)) = c
Theorem: SciLean.parametric_inverse_affine'
Proof state before:
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ f : X → R
c : R
hf : IsAffineMap R f
h : f = fun x => ⟪∇ f 0, x⟫_R + f 0
⊢ ∀ (x₁ : DataArrayN R (Fin (card ι - 1))), f ((planeDecomposition (∇ f 0) ⋯) ((c - f 0) / ‖∇ f 0‖₂[R], x₁)) = c
Tactic:
rw[h]
Proof state after:
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ f : X → R
c : R
hf : IsAffineMap R f
h : f = fun x => ⟪∇ f 0, x⟫_R + f 0
⊢ ∀ (x₁ : DataArrayN R (Fin (card ι - 1))),
    (fun x => ⟪∇ f 0, x⟫_R + f 0)
        ((planeDecomposition (∇ (x:=0), (⟪∇ f 0, x⟫_R + f 0)) ⋯)
          ((c - (fun x => ⟪∇ f 0, x⟫_R + f 0) 0) / ‖∇ (x:=0), (⟪∇ f 0, x⟫_R + f 0)‖₂[R], x₁)) =
      c
Theorem: SciLean.parametric_inverse_affine'
Proof state before:
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ f : X → R
c : R
hf : IsAffineMap R f
h : f = fun x => ⟪∇ f 0, x⟫_R + f 0
⊢ ∀ (x₁ : DataArrayN R (Fin (card ι - 1))),
    (fun x => ⟪∇ f 0, x⟫_R + f 0)
        ((planeDecomposition (∇ (x:=0), (⟪∇ f 0, x⟫_R + f 0)) ⋯)
          ((c - (fun x => ⟪∇ f 0, x⟫_R + f 0) 0) / ‖∇ (x:=0), (⟪∇ f 0, x⟫_R + f 0)‖₂[R], x₁)) =
      c
Tactic:
fun_trans [scalarGradient,planeDecomposition_orthogonal_dir]
Proof state after:
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ f : X → R
c : R
hf : IsAffineMap R f
h : f = fun x => ⟪∇ f 0, x⟫_R + f 0
⊢ (c - f 0) / ‖(<∂ f 0).2 1‖₂[R] * ‖(<∂ f 0).2 1‖₂[R] + f 0 = c
Theorem: SciLean.parametric_inverse_affine'
Proof state before:
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ f : X → R
c : R
hf : IsAffineMap R f
h : f = fun x => ⟪∇ f 0, x⟫_R + f 0
⊢ (c - f 0) / ‖(<∂ f 0).2 1‖₂[R] * ‖(<∂ f 0).2 1‖₂[R] + f 0 = c
Tactic:
have : ‖(<∂ f 0).2 1‖₂[R] ≠ 0 := sorry_proof
Proof state after:
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ f : X → R
c : R
hf : IsAffineMap R f
h : f = fun x => ⟪∇ f 0, x⟫_R + f 0
this : ‖(<∂ f 0).2 1‖₂[R] ≠ 0
⊢ (c - f 0) / ‖(<∂ f 0).2 1‖₂[R] * ‖(<∂ f 0).2 1‖₂[R] + f 0 = c
Theorem: SciLean.parametric_inverse_affine'
Proof state before:
R : Type
inst✝⁵ : RealScalar R
inst✝⁴ : PlainDataType R
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
X : Type
inst✝ : FinVec ι R X
f✝ f : X → R
c : R
hf : IsAffineMap R f
h : f = fun x => ⟪∇ f 0, x⟫_R + f 0
this : ‖(<∂ f 0).2 1‖₂[R] ≠ 0
⊢ (c - f 0) / ‖(<∂ f 0).2 1‖₂[R] * ‖(<∂ f 0).2 1‖₂[R] + f 0 = c
Tactic:
field_simp
Proof state after:
no goals
Theorem: SciLean.log_gaussian
Proof state before:
R : Type u_1
C : Type ?u.4719
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.4729
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiHilbert R U
μ : U
σ : R
x : U
⊢ log (gaussian μ σ x) =
    let x' := σ⁻¹ • (x - μ);
    -‖x'‖₂² / 2 - log σ - log (sqrt (2 * pi))
Tactic:
unfold gaussian
Proof state after:
R : Type u_1
C : Type ?u.4719
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.4729
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiHilbert R U
μ : U
σ : R
x : U
⊢ log
      (let x' := σ⁻¹ • (x - μ);
      1 / (σ * sqrt (2 * pi)) * exp (-‖x'‖₂² / 2)) =
    let x' := σ⁻¹ • (x - μ);
    -‖x'‖₂² / 2 - log σ - log (sqrt (2 * pi))
Theorem: SciLean.log_gaussian
Proof state before:
R : Type u_1
C : Type ?u.4719
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.4729
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiHilbert R U
μ : U
σ : R
x : U
⊢ log
      (let x' := σ⁻¹ • (x - μ);
      1 / (σ * sqrt (2 * pi)) * exp (-‖x'‖₂² / 2)) =
    let x' := σ⁻¹ • (x - μ);
    -‖x'‖₂² / 2 - log σ - log (sqrt (2 * pi))
Tactic:
simp [log_inv,log_mul,log_div,log_exp,log_one]
Proof state after:
R : Type u_1
C : Type ?u.4719
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.4729
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiHilbert R U
μ : U
σ : R
x : U
⊢ -log (sqrt (2 * pi)) + -log σ + -‖σ⁻¹ • (x - μ)‖₂² / 2 = -‖σ⁻¹ • (x - μ)‖₂² / 2 - log σ - log (sqrt (2 * pi))