ChristoffelSmooth · section of the QIQT-H book

QIQTH.ChristoffelSmooth

← all sections · ← BranchLedger · ClausiusFiniteWitness →

ChristoffelSmooth · entries 6–10 of 1000

Lemma 6 (contDiff_pd). source ↗

The partial derivative of a C^∞ scalar is C^∞. pd f i = (fun y => fderiv ℝ f y (Pi.single i 1)) (pd_eq_fderiv, valid everywhere since f is differentiable), and y ↦ fderiv ℝ f y is C^∞ (ContDiff.fderiv_right), so applying it to the constant basis covector e_i (ContDiff.clm_apply) is C^∞.

({f})\in C^{\infty} \to \forall (i : \mathrm{Fin}\,n), ({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-pd}{\partial_{{i}}({f})({y})}})\in C^{\infty}

Proof. By pd_eq_fderiv. $\square$

Used by christoffel_contDiff, riemann_contDiff, kgLagr_contDiff, kgStress_contDiff.

Lemma 7 (christoffel_contDiff). source ↗

Christoffel symbols are C^∞ — discharges hC. christoffel g gi μ ν ρ = ½·∑α gi_{μα}(∂_ν g_{αρ} + ∂_ρ g_{αν} − ∂_α g_{νρ}) is a finite sum of products of gi (C^∞ by hCgi) and partial derivatives of g (C^∞ by contDiff_pd + hCg).

(\forall (a b : \mathrm{Fin}\,n), ({\lambda y \mapsto g_{{a}{b}}({y})})\in C^{\infty}) \to (\forall (a b : \mathrm{Fin}\,n), ({\lambda y \mapsto g^{{a}{b}}({y})})\in C^{\infty}) \to \forall (\mu \nu \rho : \mathrm{Fin}\,n), ({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-christoffel}{\Gamma^{{\mu}}_{{\nu}{\rho}}({y})}})\in C^{\infty}

Proof. By contDiff_pd, pd. $\square$

Used by riemann_contDiff, qiqt_gr_freefield_localized', qiqt_bekenstein_gives_gr.

Lemma 8 (riemann_contDiff). source ↗

The Riemann tensor is C^∞ — R^ρ_{σμν} = ∂_μΓ^ρ_{νσ} − ∂_νΓ^ρ_{μσ} + Σ_l(Γ^ρ_{μl}Γ^l_{νσ} − Γ^ρ_{νl}Γ^l_{μσ}) is a finite combination of ∂Γ (contDiff_pd ∘ christoffel_contDiff) and ΓΓ.

(\forall (a b : \mathrm{Fin}\,n), ({\lambda y \mapsto g_{{a}{b}}({y})})\in C^{\infty}) \to (\forall (a b : \mathrm{Fin}\,n), ({\lambda y \mapsto g^{{a}{b}}({y})})\in C^{\infty}) \to \forall (\rho \sigma \mu \nu : \mathrm{Fin}\,n), ({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-riemann}{\mathrm{Riem}}\,g\,\mathrm{gi}\,\rho\,\sigma\,\mu\,\nu\,y})\in C^{\infty}

Proof. By contDiff_pd, christoffel_contDiff, pd, christoffel. $\square$

Used by ricci_contDiff.

Lemma 9 (ricci_contDiff). source ↗

The Ricci tensor is C^∞ — R_{σν} = ∑μ R^μ_{σμν} (sum of C^∞ Riemann components).

(\forall (a b : \mathrm{Fin}\,n), ({\lambda y \mapsto g_{{a}{b}}({y})})\in C^{\infty}) \to (\forall (a b : \mathrm{Fin}\,n), ({\lambda y \mapsto g^{{a}{b}}({y})})\in C^{\infty}) \to \forall (\sigma \nu : \mathrm{Fin}\,n), ({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-ricci}{R_{{\sigma}{\nu}}({y})}})\in C^{\infty}

Proof. By riemann_contDiff, riemann. $\square$

Used by scalarCurv_contDiff.

Lemma 10 (scalarCurv_contDiff). source ↗

The scalar curvature is C^∞ — R = ∑_{σν} g^{σν} R_{σν} (a finite combination of C^∞ gi and C^∞ Ricci). Feeds the hreg regularity input of the QIQT→GR capstone (Tier A4).

(\forall (a b : \mathrm{Fin}\,n), ({\lambda y \mapsto g_{{a}{b}}({y})})\in C^{\infty}) \to (\forall (a b : \mathrm{Fin}\,n), ({\lambda y \mapsto g^{{a}{b}}({y})})\in C^{\infty}) \to ({\lambda y \mapsto \href{/browser/qiqth-curvature#d-qiqth-curvature-scalarcurv}{R({y})}})\in C^{\infty}

Proof. By ricci_contDiff, ricci. $\square$

Used by hreg_kg.

← all sections · ← BranchLedger · ClausiusFiniteWitness →