Skip to content

Commit

Permalink
fixes #1357
Browse files Browse the repository at this point in the history
  • Loading branch information
affeldt-aist committed Oct 24, 2024
1 parent 253f6a1 commit 00d57eb
Show file tree
Hide file tree
Showing 2 changed files with 60 additions and 65 deletions.
107 changes: 51 additions & 56 deletions theories/derive.v
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ Lemma diffE (F : filter_on V) (f : V -> W) :
Proof. by move=> /diffP []. Qed.

Lemma littleo_center0 (x : V) (f : V -> W) (e : V -> V) :
[o_x e of f] = [o_ (0 : V) (e \o shift x) of f \o shift x] \o center x.
[o_x e of f] = [o_ 0 (e \o shift x) of f \o shift x] \o center x.
Proof.
rewrite /the_littleo /insubd /=; have [g /= _ <-{f}|/asboolP Nfe] /= := insubP.
rewrite insubT //= ?comp_shiftK //; apply/asboolP => _/posnumP[eps].
Expand All @@ -128,7 +128,7 @@ Hint Extern 0 (continuous _) => exact: diff_continuous : core.

Lemma diff_locallyxP (x : V) (f : V -> W) :
differentiable f x <-> continuous ('d f x) /\
forall h, f (h + x) = f x + 'd f x h +o_(h \near 0 : V) h.
forall h, f (h + x) = f x + 'd f x h +o_(h \near 0) h.
Proof.
split=> [dxf|[dfc dxf]].
split => //; apply: eqaddoEx => h; have /diffE -> := dxf.
Expand All @@ -141,20 +141,20 @@ by rewrite -[_ (y - x)]/((_ \o (center x)) y) -littleo_center0.
Qed.

Lemma diff_locallyx (x : V) (f : V -> W) : differentiable f x ->
forall h, f (h + x) = f x + 'd f x h +o_(h \near 0 : V) h.
forall h, f (h + x) = f x + 'd f x h +o_(h \near 0) h.
Proof. by move=> /diff_locallyxP []. Qed.

Lemma diff_locallyxC (x : V) (f : V -> W) : differentiable f x ->
forall h, f (x + h) = f x + 'd f x h +o_(h \near 0 : V) h.
forall h, f (x + h) = f x + 'd f x h +o_(h \near 0) h.
Proof. by move=> ?; apply/eqaddoEx => h; rewrite [x + h]addrC diff_locallyx. Qed.

Lemma diff_locallyP (x : V) (f : V -> W) :
differentiable f x <->
continuous ('d f x) /\ (f \o shift x = cst (f x) + 'd f x +o_ (0 : V) id).
continuous ('d f x) /\ (f \o shift x = cst (f x) + 'd f x +o_ 0 id).
Proof. by apply: iff_trans (diff_locallyxP _ _) _; rewrite funeqE. Qed.

Lemma diff_locally (x : V) (f : V -> W) : differentiable f x ->
(f \o shift x = cst (f x) + 'd f x +o_ (0 : V) id).
(f \o shift x = cst (f x) + 'd f x +o_ 0 id).
Proof. by move=> /diff_locallyP []. Qed.

End Differential_numFieldType.
Expand Down Expand Up @@ -198,7 +198,6 @@ by apply/eqolim0P; apply: (cvg_trans (dfc 0)); rewrite linear0.
Unshelve. all: by end_near. Qed.

Section littleo_lemmas.

Variables (X Y Z : normedModType R).

Lemma normm_littleo x (f : X -> Y) : `| [o_(x \near x) (1 : R) of f x]| = 0.
Expand All @@ -209,7 +208,7 @@ by move=> /implyP; case : real_ltgtP; rewrite ?realE ?normrE //= lexx.
Qed.

Lemma littleo_lim0 (f : X -> Y) (h : _ -> Z) (x : X) :
f @ x --> (0 : Y) -> [o_x f of h] x = 0.
f @ x --> 0 -> [o_x f of h] x = 0.
Proof.
move/eqolim0P => ->; have [k /(_ _ [gt0 of 1 : R])/=] := littleo.
by move=> /nbhs_singleton; rewrite mul1r normm_littleo normr_le0 => /eqP.
Expand All @@ -225,7 +224,7 @@ Section diff_locally_converse_tentative.
(* and thus a littleo of 1, and so is id *)
(* This can be generalized to any dimension *)
Lemma diff_locally_converse_part1 (f : R -> R) (a b x : R) :
f \o shift x = cst a + b *: idfun +o_ (0 : R) id -> f x = a.
f \o shift x = cst a + b *: idfun +o_ 0 id -> f x = a.
Proof.
rewrite funeqE => /(_ 0) /=; rewrite add0r => ->.
by rewrite -[LHS]/(_ 0 + _ 0 + _ 0) /cst [X in a + X]scaler0 littleo_lim0 ?addr0.
Expand All @@ -250,7 +249,7 @@ Class is_derive (a v : V) (f : V -> W) (df : W) := DeriveDef {
Lemma derivable_nbhs (f : V -> W) a v :
derivable f a v ->
(fun h => (f \o shift a) (h *: v)) = (cst (f a)) +
(fun h => h *: ('D_v f a)) +o_ (nbhs (0 :R)) id.
(fun h => h *: ('D_v f a)) +o_ (nbhs 0) id.
Proof.
move=> df; apply/eqaddoP => _/posnumP[e].
rewrite -nbhs_nearE nbhs_simpl /= dnbhsE; split; last first.
Expand All @@ -270,7 +269,7 @@ Unshelve. all: by end_near. Qed.
Lemma derivable_nbhsP (f : V -> W) a v :
derivable f a v <->
(fun h => (f \o shift a) (h *: v)) = (cst (f a)) +
(fun h => h *: ('D_v f a)) +o_ (nbhs (0 : R)) id.
(fun h => h *: ('D_v f a)) +o_ (nbhs 0) id.
Proof.
split; first exact: derivable_nbhs.
move=> df; apply/cvg_ex; exists ('D_v f a).
Expand All @@ -286,15 +285,15 @@ Unshelve. all: by end_near. Qed.

Lemma derivable_nbhsx (f : V -> W) a v :
derivable f a v -> forall h, f (a + h *: v) = f a + h *: 'D_v f a
+o_(h \near (nbhs (0 : R))) h.
+o_(h \near (nbhs 0)) h.
Proof.
move=> /derivable_nbhs; rewrite funeqE => df.
by apply: eqaddoEx => h; have /= := (df h); rewrite addrC => ->.
Qed.

Lemma derivable_nbhsxP (f : V -> W) a v :
derivable f a v <-> forall h, f (a + h *: v) = f a + h *: 'D_v f a
+o_(h \near (nbhs (0 :R))) h.
+o_(h \near nbhs 0) h.
Proof.
split; first exact: derivable_nbhsx.
move=> df; apply/derivable_nbhsP; apply/eqaddoE; rewrite funeqE => h.
Expand Down Expand Up @@ -397,7 +396,7 @@ Section DifferentialR3.
Variable R : numFieldType.

Fact dcst (V W : normedModType R) (a : W) (x : V) : continuous (0 : V -> W) /\
cst a \o shift x = cst (cst a x) + \0 +o_ (0 : V) id.
cst a \o shift x = cst (cst a x) + \0 +o_ 0 id.
Proof.
split; first exact: cst_continuous.
apply/eqaddoE; rewrite addr0 funeqE => ? /=; rewrite -[LHS]addr0; congr (_ + _).
Expand All @@ -409,7 +408,7 @@ Variables (V W : normedModType R).
Fact dadd (f g : V -> W) x :
differentiable f x -> differentiable g x ->
continuous ('d f x \+ 'd g x) /\
(f + g) \o shift x = cst ((f + g) x) + ('d f x \+ 'd g x) +o_ (0 : V) id.
(f + g) \o shift x = cst ((f + g) x) + ('d f x \+ 'd g x) +o_ 0 id.
Proof.
move=> df dg; split => [?|]; do ?exact: continuousD.
apply/(@eqaddoE R); rewrite funeqE => y /=; rewrite -[(f + g) _]/(_ + _).
Expand All @@ -418,7 +417,7 @@ Qed.

Fact dopp (f : V -> W) x :
differentiable f x -> continuous (- ('d f x : V -> W)) /\
(- f) \o shift x = cst (- f x) \- 'd f x +o_ (0 : V) id.
(- f) \o shift x = cst (- f x) \- 'd f x +o_ 0 id.
Proof.
move=> df; split; first by move=> ?; apply: continuousN.
apply/eqaddoE; rewrite funeqE => y /=.
Expand All @@ -431,7 +430,7 @@ Proof. by move=> ? <-. Qed.

Fact dscale (f : V -> W) k x :
differentiable f x -> continuous (k \*: 'd f x) /\
(k *: f) \o shift x = cst ((k *: f) x) + k \*: 'd f x +o_ (0 : V) id.
(k *: f) \o shift x = cst ((k *: f) x) + k \*: 'd f x +o_ 0 id.
Proof.
move=> df; split; first by move=> ?; apply: continuousZr.
apply/eqaddoE; rewrite funeqE => y /=.
Expand All @@ -443,7 +442,7 @@ Fact dscalel (k : V -> R) (f : W) x :
differentiable k x ->
continuous (fun z : V => 'd k x z *: f) /\
(fun z => k z *: f) \o shift x =
cst (k x *: f) + (fun z => 'd k x z *: f) +o_ (0 : V) id.
cst (k x *: f) + (fun z => 'd k x z *: f) +o_ 0 id.
Proof.
move=> df; split.
move=> ?; exact/continuousZl/diff_continuous.
Expand All @@ -452,7 +451,7 @@ by rewrite diff_locallyx //= !scalerDl scaleolx.
Qed.

Fact dlin (V' W' : normedModType R) (f : {linear V' -> W'}) x :
continuous f -> f \o shift x = cst (f x) + f +o_ (0 : V') id.
continuous f -> f \o shift x = cst (f x) + f +o_ 0 id.
Proof.
move=> df; apply: eqaddoE; rewrite funeqE => y /=.
rewrite linearD addrC -[LHS]addr0; congr (_ + _).
Expand All @@ -462,11 +461,11 @@ Qed.
(* TODO: generalize *)
Lemma compoO_eqo (U V' W' : normedModType R) (f : U -> V')
(g : V' -> W') :
[o_ (0 : V') id of g] \o [O_ (0 : U) id of f] =o_ (0 : U) id.
[o_ 0 id of g] \o [O_ 0 id of f] =o_ 0 id.
Proof.
apply/eqoP => _ /posnumP[e].
have /bigO_exP [_ /posnumP[k]] := bigOP [bigO of [O_ (0 : U) id of f]].
have := littleoP [littleo of [o_ (0 : V') id of g]].
have /bigO_exP [_ /posnumP[k]] := bigOP [bigO of [O_ 0 id of f]].
have := littleoP [littleo of [o_ 0 id of g]].
move=> /(_ (e%:num / k%:num)) /(_ _) /nbhs_ballP [//|_ /posnumP[d] hd].
apply: filter_app; near=> x => leOxkx; apply: le_trans (hd _ _) _; last first.
rewrite -ler_pdivlMl //; apply: le_trans leOxkx _.
Expand All @@ -476,19 +475,18 @@ Unshelve. all: by end_near. Qed.

Lemma compoO_eqox (U V' W' : normedModType R) (f : U -> V')
(g : V' -> W') :
forall x : U, [o_ (0 : V') id of g] ([O_ (0 : U) id of f] x) =o_(x \near 0 : U) x.
forall x : U, [o_ 0 id of g] ([O_ 0 id of f] x) =o_(x \near 0) x.
Proof. by move=> x; rewrite -[LHS]/((_ \o _) x) compoO_eqo. Qed.

(* TODO: generalize *)
Lemma compOo_eqo (U V' W' : normedModType R) (f : U -> V')
(g : V' -> W') :
[O_ (0 : V') id of g] \o [o_ (0 : U) id of f] =o_ (0 : U) id.
Lemma compOo_eqo (U V' W' : normedModType R) (f : U -> V') (g : V' -> W') :
[O_ 0 id of g] \o [o_ 0 id of f] =o_ 0 id.
Proof.
apply/eqoP => _ /posnumP[e].
have /bigO_exP [_ /posnumP[k]] := bigOP [bigO of [O_ (0 : V') id of g]].
have /bigO_exP [_ /posnumP[k]] := bigOP [bigO of [O_ 0 id of g]].
move=> /nbhs_ballP [_ /posnumP[d] hd].
have ekgt0 : e%:num / k%:num > 0 by [].
have /(_ _ ekgt0) := littleoP [littleo of [o_ (0 : U) id of f]].
have /(_ _ ekgt0) := littleoP [littleo of [o_ 0 id of f]].
apply: filter_app; near=> x => leoxekx; apply: le_trans (hd _ _) _; last first.
by rewrite -ler_pdivlMl // mulrA [_^-1 * _]mulrC.
by rewrite -ball_normE /= distrC subr0 (le_lt_trans leoxekx)// -ltr_pdivlMl //.
Expand All @@ -500,7 +498,7 @@ Section DifferentialR3_numFieldType.
Variable R : numFieldType.

Lemma littleo_linear0 (V W : normedModType R) (f : {linear V -> W}) :
(f : V -> W) =o_ (0 : V) id -> f = cst 0 :> (V -> W).
(f : V -> W) =o_ 0 id -> f = cst 0 :> (V -> W).
Proof.
move/eqoP => oid.
rewrite funeqE => x; apply/eqP; have [|xn0] := real_le0P (normr_real x).
Expand All @@ -520,14 +518,13 @@ Qed.

Lemma diff_unique (V W : normedModType R) (f : V -> W)
(df : {linear V -> W}) x :
continuous df -> f \o shift x = cst (f x) + df +o_ (0 : V) id ->
continuous df -> f \o shift x = cst (f x) + df +o_ 0 id ->
'd f x = df :> (V -> W).
Proof.
move=> dfc dxf; apply/subr0_eq; rewrite -[LHS]/(_ \- _).
apply/littleo_linear0/eqoP/eq_some_oP => /=; rewrite funeqE => y /=.
have hdf h :
(f \o shift x = cst (f x) + h +o_ (0 : V) id) ->
h = f \o shift x - cst (f x) +o_ (0 : V) id.
have hdf h : (f \o shift x = cst (f x) + h +o_ 0 id) ->
h = f \o shift x - cst (f x) +o_ 0 id.
move=> hdf; apply: eqaddoE.
rewrite hdf addrAC -!addrA addrC !addrA subrK.
rewrite -[LHS]addr0 -addrA; congr (_ + _).
Expand Down Expand Up @@ -712,25 +709,24 @@ by rewrite invf_div mul1r [ltRHS]splitr; apply: ltr_pwDr.
Qed.

Lemma linear_eqO (V' W' : normedModType R) (f : {linear V' -> W'}) :
continuous f -> (f : V' -> W') =O_ (0 : V') id.
continuous f -> (f : V' -> W') =O_ 0 id.
Proof.
move=> /linear_lipschitz [k kgt0 flip]; apply/eqO_exP; exists k => //.
exact: filterE.
Qed.

Lemma diff_eqO (V' W' : normedModType R) (x : filter_on V') (f : V' -> W') :
differentiable f x -> ('d f x : V' -> W') =O_ (0 : V') id.
differentiable f x -> ('d f x : V' -> W') =O_ 0 id.
Proof. by move=> /diff_continuous /linear_eqO; apply. Qed.

Lemma compOo_eqox (U V' W' : normedModType R) (f : U -> V')
(g : V' -> W') : forall x,
[O_ (0 : V') id of g] ([o_ (0 : U) id of f] x) =o_(x \near 0 : U) x.
Proof. by move=> x; rewrite -[LHS]/((_ \o _) x) compOo_eqo. Qed.
Lemma compOo_eqox (U V' W' : normedModType R) (f : U -> V') (g : V' -> W') x :
[O_ 0 id of g] ([o_ 0 id of f] x) =o_(x \near 0) x.
Proof. by rewrite -[LHS]/((_ \o _) x) compOo_eqo. Qed.

Fact dcomp (U V' W' : normedModType R) (f : U -> V') (g : V' -> W') x :
differentiable f x -> differentiable g (f x) ->
continuous ('d g (f x) \o 'd f x) /\ forall y,
g (f (y + x)) = g (f x) + ('d g (f x) \o 'd f x) y +o_(y \near 0 : U) y.
g (f (y + x)) = g (f x) + ('d g (f x) \o 'd f x) y +o_(y \near 0) y.
Proof.
move=> df dg; split; first by move=> ?; apply: continuous_comp.
apply: eqaddoEx => y; rewrite diff_locallyx// -addrA diff_locallyxC// linearD.
Expand Down Expand Up @@ -792,7 +788,7 @@ by rewrite prod_normE/= !normrZ !normfV !normr_id !mulVf ?gt_eqF// maxxx ltr1n.
Qed.

Lemma bilinear_eqo (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) :
continuous (fun p => f p.1 p.2) -> (fun p => f p.1 p.2) =o_ (0 : U * V') id.
continuous (fun p => f p.1 p.2) -> (fun p => f p.1 p.2) =o_ 0 id.
Proof.
move=> fc; have [_ /posnumP[k] fschwarz] := bilinear_schwarz fc.
apply/eqoP=> _ /posnumP[e]; near=> x; rewrite (le_trans (fschwarz _ _))//.
Expand All @@ -807,7 +803,7 @@ Fact dbilin (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) p :
continuous (fun p => f p.1 p.2) ->
continuous (fun q => (f p.1 q.2 + f q.1 p.2)) /\
(fun q => f q.1 q.2) \o shift p = cst (f p.1 p.2) +
(fun q => f p.1 q.2 + f q.1 p.2) +o_ (0 : U * V') id.
(fun q => f p.1 q.2 + f q.1 p.2) +o_ 0 id.
Proof.
move=> fc; split=> [q|].
by apply: (@continuousD _ _ _ (fun q => f p.1 q.2) (fun q => f q.1 p.2));
Expand Down Expand Up @@ -870,16 +866,16 @@ Fact dpair (U V' W' : normedModType R) (f : U -> V') (g : U -> W') x :
differentiable f x -> differentiable g x ->
continuous (fun y => ('d f x y, 'd g x y)) /\
(fun y => (f y, g y)) \o shift x = cst (f x, g x) +
(fun y => ('d f x y, 'd g x y)) +o_ (0 : U) id.
(fun y => ('d f x y, 'd g x y)) +o_ 0 id.
Proof.
move=> df dg; split=> [?|]; first by apply: cvg_pair; apply: diff_continuous.
apply/eqaddoE; rewrite funeqE => y /=.
rewrite ![_ (_ + x)]diff_locallyx//.
(* fixme *)
have -> : forall h e, (f x + 'd f x y + [o_ (0 : U) id of h] y,
g x + 'd g x y + [o_ (0 : U) id of e] y) =
have -> : forall h e, (f x + 'd f x y + [o_ 0 id of h] y,
g x + 'd g x y + [o_ 0 id of e] y) =
(f x, g x) + ('d f x y, 'd g x y) +
([o_ (0 : U) id of h] y, [o_ (0 : U) id of e] y) by [].
([o_ 0 id of h] y, [o_ 0id of e] y) by [].
by congr (_ + _); rewrite -[LHS]/((fun y => (_ y, _ y)) y) eqo_pair.
Qed.

Expand Down Expand Up @@ -929,16 +925,15 @@ Lemma differentiableM (f g : V -> R) x :
differentiable f x -> differentiable g x -> differentiable (f * g) x.
Proof. by move=> /differentiableP df /differentiableP dg. Qed.

(* fixme using *)
(* (1 / (h + x) - 1 / x) / h = - 1 / (h + x) x = -1/x^2 + o(1) *)
(* TODO: fixme using (1 / (h + x) - 1 / x) / h = - 1 / (h + x) x = -1/x^2 + o(1) *)
Fact dinv (x : R) :
x != 0 -> continuous (fun h : R => - x ^- 2 *: h) /\
(fun x => x^-1)%R \o shift x = cst (x^-1)%R +
(fun h : R => - x ^- 2 *: h) +o_ (0 : R) id.
(fun h : R => - x ^- 2 *: h) +o_ 0 id.
Proof.
move=> xn0; suff: continuous (fun h : R => - (1 / x) ^+ 2 *: h) /\
(fun x => 1 / x ) \o shift x = cst (1 / x) +
(fun h : R => - (1 / x) ^+ 2 *: h) +o_ (0 : R) id.
(fun h : R => - (1 / x) ^+ 2 *: h) +o_ 0 id.
rewrite !mul1r !GRing.exprVn.
rewrite (_ : (fun x => x^-1) = (fun x => 1 / x ))//.
by rewrite funeqE => y; rewrite mul1r.
Expand Down Expand Up @@ -1031,7 +1026,7 @@ Variables (R : numFieldType) (U : normedModType R).
Implicit Types f : R -> U.

Let der1 f x : derivable f x 1 ->
f \o shift x = cst (f x) + ( *:%R^~ (f^`() x)) +o_ (0 : R) id.
f \o shift x = cst (f x) + ( *:%R^~ (f^`() x)) +o_ 0 id.
Proof.
move=> df; apply/eqaddoE; have /derivable_nbhsP := df.
have -> : (fun h => (f \o shift x) h%:A) = f \o shift x.
Expand Down Expand Up @@ -1214,7 +1209,7 @@ Proof. by move=> /derivableP df /derivableP dg. Qed.

Fact der_scal f (k : R) (x v : V) : derivable f x v ->
(fun h => h^-1 *: ((k \*: f \o shift x) (h *: v) - (k \*: f) x)) @
(0 : R)^' --> k *: 'D_v f x.
0^' --> k *: 'D_v f x.
Proof.
move=> df; evar (h : R -> W); rewrite [X in X @ _](_ : _ = h) /=; last first.
rewrite funeqE => r.
Expand Down Expand Up @@ -1272,7 +1267,7 @@ Implicit Types f g : V -> R.
Fact der_mult f g (x v : V) :
derivable f x v -> derivable g x v ->
(fun h => h^-1 *: (((f * g) \o shift x) (h *: v) - (f * g) x)) @
(0 : R)^' --> f x *: 'D_v g x + g x *: 'D_v f x.
0^' --> f x *: 'D_v g x + g x *: 'D_v f x.
Proof.
move=> df dg.
evar (fg : R -> R); rewrite [X in X @ _](_ : _ = fg) /=; last first.
Expand Down Expand Up @@ -1337,17 +1332,17 @@ Proof. by move=> /derivableP df; rewrite derive_val. Qed.

Fact der_inv f (x v : V) : f x != 0 -> derivable f x v ->
(fun h => h^-1 *: (((fun y => (f y)^-1) \o shift x) (h *: v) - (f x)^-1)) @
(0 : R)^' --> - (f x) ^-2 *: 'D_v f x.
0^' --> - (f x) ^-2 *: 'D_v f x.
Proof.
move=> fxn0 df.
have /derivable1P/derivable1_diffP/differentiable_continuous := df.
move=> /continuous_withinNx; rewrite scale0r add0r => fc.
have fn0 : (0 : R)^' [set h | f (h *: v + x) != 0].
have fn0 : 0^' [set h | f (h *: v + x) != 0].
apply: (fc [set x | x != 0]); exists `|f x|; first by rewrite /= normr_gt0.
move=> y; rewrite /= => yltfx.
by apply/eqP => y0; move: yltfx; rewrite y0 subr0 ltxx.
have : (fun h => - ((f x)^-1 * (f (h *: v + x))^-1) *:
(h^-1 *: (f (h *: v + x) - f x))) @ (0 : R)^' -->
(h^-1 *: (f (h *: v + x) - f x))) @ 0^' -->
- (f x) ^- 2 *: 'D_v f x.
by apply: cvgM => //; apply: cvgN; rewrite expr2 invfM; apply: cvgM;
[exact: cvg_cst| exact: cvgV].
Expand Down
Loading

0 comments on commit 00d57eb

Please sign in to comment.