On this page

GaussianAnalysisgaussianpartial_derivative

Continuous partial derivatives

GaussianAnalysis.gaussian.partial_derivativelibrary/gaussian/partial_derivative.v173 lines11 lemmas and theorems, 1 definitionsource

Imports 2 library modules and 15 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.algebra.arithmetic_tactic, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.reals.reals, mathcomp.algebra.interval, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.landau, mathcomp.analysis.derive

Imported by 6

A function F : 'rV[R]_n -> R whose partial derivatives 'D_(delta_mx 0 j) F exist everywhere and are continuous is differentiable, and its differential is v |-> \sum_j v 0 j * 'D_(delta_mx 0 j) F x (differentiable_partials, diff_partials). The proof writes the increment of F as a sum of increments along the coordinates and applies the mean value theorem to each (mean_value_coord, partials_expansion).

rV_prefix k h the row vector h with its coordinates of index k or more set to 0

Main results

Results	Statement
differentiable_partialsdiff_partials	A function on `'rV[R]_n` whose partial derivatives exist everywhere and are continuous is differentiable, with differential `v \|-> \sum_j v_j d_j F x`.

Declarations12 exported

sectionpartials

Context {R : realType} {n : nat}.
Variables (F : 'rV[R]_n -> R) (DF : 'I_n -> 'rV[R]_n -> R).
Hypothesis F_partial : forall j x, is_derive x (delta_mx 0 j) F (DF j x).
Hypothesis DF_cont : forall j, continuous (DF j).

definition rV_prefix source, line 41

Type

forall {R : realType} {n : nat}, nat -> 'rV_n -> 'rV_n

Definition

Definition rV_prefix k (h : 'rV[R]_n) : 'rV[R]_n :=
  \row_j (if (j < k)%N then h 0 j else 0).

The first k coordinates of h, the others set to 0.

Used by 5 declarations in 1 file

this file: rV_prefix0, rV_prefixn, rV_prefixS, rV_prefix_norm, partials_expansion

lemma rV_prefix0 source, line 44

forall {R : realType} {n : nat} (h : 'rV_n), rV_prefix 0 h = 0

Statement as written in the source

Lemma rV_prefix0 h : rV_prefix 0 h = 0.

Used by 1 declaration in 1 file

this file: partials_expansion

lemma rV_prefixn source, line 47

forall {R : realType} {n : nat} (h : 'rV_n), rV_prefix n h = h

Statement as written in the source

Lemma rV_prefixn h : rV_prefix n h = h.

Used by 1 declaration in 1 file

this file: partials_expansion

lemma rV_prefixS source, line 50

forall {R : realType} {n : nat} (h : 'rV_n) (k : 'I_n),
rV_prefix k.+1 h = h 0 k *: delta_mx 0 k + rV_prefix k h

Statement as written in the source

Lemma rV_prefixS h (k : 'I_n) :
  rV_prefix k.+1 h = h 0 k *: delta_mx 0 k + rV_prefix k h.

Used by 1 declaration in 1 file

this file: partials_expansion

lemma rV_prefix_norm source, line 58

forall {R : realType} {n : nat} [h : 'rV_n] [k : 'I_n] [c : R],
`|c| <= `|h 0 k| -> `|c *: delta_mx 0 k + rV_prefix k h| <= `|h|

Statement as written in the source

Lemma rV_prefix_norm (h : 'rV[R]_n) (k : 'I_n) (c : R) : `|c| <= `|h 0 k| ->
  `|c *: delta_mx 0 k + rV_prefix k h| <= `|h|.

Used by 1 declaration in 1 file

this file: partials_expansion

lemma mean_value_coord source, line 71

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R],
(forall (j : 'I_n)
   (x : 'rV[R]_n),
 is_derive x (delta_mx 0 j) F (DF j x)) ->
forall (x : 'rV_n) (j : 'I_n) (t : R),
exists2 c : R,
  `|c| <= `|t| & F (t *: delta_mx 0 j + x) - F x = t * DF j (c *: delta_mx 0 j + x)

Statement as written in the source

Lemma mean_value_coord (x : 'rV[R]_n) (j : 'I_n) (t : R) :
  exists2 c : R, `|c| <= `|t| &
    F (t *: delta_mx 0 j + x) - F x = t * DF j (c *: delta_mx 0 j + x).

Used by 1 declaration in 1 file

this file: partials_expansion

lemma partials_expansion source, line 99

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R],
(forall (j : 'I_n)
   (x : 'rV[R]_n),
 is_derive x (delta_mx 0 j) F (DF j x)) ->
(forall j : 'I_n, continuous (DF j)) ->
forall x : 'rV_n,
(fun h : 'rV_n => F (h + x) - F x - \sum_(j < n) h 0 j * DF j x) =o_
(0 : 'rV_n) id

Statement as written in the source

Lemma partials_expansion (x : 'rV[R]_n) :
  (fun h : 'rV[R]_n => F (h + x) - F x - \sum_(j < n) h 0 j * DF j x)
    =o_ (0 : 'rV[R]_n) id.

Used by 1 declaration in 1 file

this file: partials_diff_differentiable

lemma partials_linear source, line 135

forall {R : realType} {n : nat} (DF : 'I_n -> 'rV_n -> R) (x : 'rV_n),
linear (fun v : 'rV_n => \sum_(j < n) v 0 j * DF j x)

Statement as written in the source

Lemma partials_linear (x : 'rV[R]_n) :
  linear (fun v : 'rV[R]_n => \sum_(j < n) v 0 j * DF j x).

Used by 1 declaration in 1 file

this file: partials_diff_differentiable

lemma continuous_partials_linear source, line 142

forall {R : realType} {n : nat} [DF : 'I_n -> 'rV_n -> R] [x : 'rV_n],
continuous (fun v : 'rV_n => \sum_(j < n) v 0 j * DF j x)

Statement as written in the source

Lemma continuous_partials_linear (x : 'rV[R]_n) :
  continuous (fun v : 'rV[R]_n => \sum_(j < n) v 0 j * DF j x).

Used by 1 declaration in 1 file

this file: partials_diff_differentiable

lemma partials_diff_differentiable source, line 149

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R],
(forall (j : 'I_n)
   (x : 'rV[R]_n),
 is_derive x (delta_mx 0 j) F (DF j x)) ->
(forall j : 'I_n, continuous (DF j)) ->
forall x : 'rV_n,
differentiable F x /\ 'd F x = (fun v : 'rV_n => \sum_(j < n) v 0 j * DF j x)

Statement as written in the source

Lemma partials_diff_differentiable (x : 'rV[R]_n) :
  differentiable F x /\
  'd F x = (fun v : 'rV[R]_n => \sum_(j < n) v 0 j * DF j x) :> ('rV[R]_n -> R).

Used by 2 declarations in 1 file

this file: differentiable_partials, diff_partials

lemma differentiable_partials main result source, line 166

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R],
(forall (j : 'I_n)
   (x : 'rV[R]_n),
 is_derive x (delta_mx 0 j) F (DF j x)) ->
(forall j : 'I_n, continuous (DF j)) -> forall x : 'rV_n, differentiable F x

Main result, as the README states it

A function on 'rV[R]_n whose partial derivatives exist everywhere and are continuous is differentiable, with differential v |-> \sum_j v_j d_j F x.

Statement as written in the source

Lemma differentiable_partials (x : 'rV[R]_n) : differentiable F x.

Used by 10 declarations in 5 files

GaussianAnalysis.gaussian.gauss_interpolation: DF_diff, F_diff
GaussianAnalysis.comparison.gauss_smoothing: lipschitz_frobenius_grad, gauss_smooth_differentiable
GaussianAnalysis.comparison.gauss_concentration: herbst_Fdiff, gauss_concentration_smooth
GaussianAnalysis.comparison.slepian: lse_differentiable, softmax_differentiable
GaussianAnalysis.comparison.gordon: smm_D_differentiable, smm_differentiable

lemma diff_partials main result source, line 169

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R],
(forall (j : 'I_n)
   (x : 'rV[R]_n),
 is_derive x (delta_mx 0 j) F (DF j x)) ->
(forall j : 'I_n, continuous (DF j)) ->
forall x : 'rV_n, 'd F x = (fun v : 'rV_n => \sum_(j < n) v 0 j * DF j x)

Main result

Stated in the README together with differentiable_partials.

Statement as written in the source

Lemma diff_partials (x : 'rV[R]_n) :
  'd F x = (fun v : 'rV[R]_n => \sum_(j < n) v 0 j * DF j x) :> ('rV[R]_n -> R).

Used by 1 declaration in 1 file

GaussianAnalysis.comparison.gauss_smoothing: lipschitz_frobenius_grad

Generated from commit 9046883 (tag phase12) of the ellipsoid fitting repository. Signatures are printed by Rocq 9.1.1; links in the source statements come from the compiled .glob files. The source links open the files on GitHub at this commit, in the now-public repository.