Formule de Stokes sur un ouvert du demi-espace

La différentielle. Dans $d(f_i\,dz_{\hat\imath}) = \sum_j \partial_j f_i\,dz_j \wedge dz_{\hat\imath}$, seul le terme $j = i$ subsiste, et ramener $dz_i$ à sa place coûte $i - 1$ transpositions, comme dans la preuve du nœud Formule de Stokes : le signe $(-1)^{i-1}$ se compense.

Prolongement. Le prolongement $\hat f_i$ de $f_i$ par $0$ à $\mathbb H^n$ est de classe $C^\infty$, au sens du nœud Variétés à bord : il l'est sur l'ouvert $A$ et sur l'ouvert $\mathbb H^n \setminus K$ de $\mathbb H^n$, où il est nul, $K$ étant fermé ; ses dérivées partielles sont les prolongements par $0$ de celles de $f_i$. Le compact $K$ est borné : soit $P = P' \times [0, b]$, avec $P' = \prod_{l < n}[a_l, b_l]$, un pavé tel que $K \subset \prod_{l < n}\,]a_l, b_l[ \times [0, b[$. La fonction $z' \mapsto f_n(z', 0)$ est continue sur $A'$ et nulle hors du compact $\{z' : (z', 0) \in K\}$ : elle appartient à $C_c(A')$, et son intégrale est celle de $z' \mapsto \hat f_n(z', 0)$ sur $P'$.

Les directions tangentes. Soit $i < n$. Par le nœud Fubini pour les fonctions continues, (iii), on peut intégrer d'abord par rapport à $z_i$. Les autres variables étant fixées, la fonction $t \mapsto \hat f_i(z_1, \dots, t, \dots, z_n)$ est de classe $C^1$ sur $[a_i, b_i]$, de dérivée $\partial_i\hat f_i$ : la droite parcourue reste dans $\mathbb H^n$, où $\hat f_i$ coïncide avec ses prolongements locaux. Elle est nulle en $a_i$ et en $b_i$, et le théorème fondamental (Théorème fondamental) donne $\int_{a_i}^{b_i} \partial_i\hat f_i = 0$. Donc $\int_P \partial_i\hat f_i = 0$.

La direction normale. Intégrons d'abord par rapport à $z_n$, sur $[0, b]$. Pour $z'$ fixé, la fonction $u(t) = \hat f_n(z', t)$ est continue sur $[0, b]$, dérivable sur $]0, b[$, de dérivée $\partial_n\hat f_n(z', t)$, fonction continue sur $[0, b]$. La fonction $t \mapsto \int_0^t \partial_n\hat f_n(z', s)\,ds - u(t)$ est continue sur $[0, b]$, de dérivée nulle sur $]0, b[$ : elle est constante (Signe de la dérivée, (ii)). Comme $u(b) = 0$, $$\int_0^b \partial_n\hat f_n(z', t)\,dt = -\hat f_n(z', 0).$$ En intégrant sur $P'$, on obtient $\int_P \partial_n\hat f_n = -\int_{P'} \hat f_n(z', 0)\,dz'$, et la somme sur $i$ donne la formule. Pour $n = 1$, $P = [0, b]$, et la direction normale est la seule : on trouve $-\hat f_1(0)$.