noncomputable def ChristoffelSymbols.secondPartialDeriv {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (i j : Fin n) : Fin (n + 1) → ℝ

noncomputable def ChristoffelSymbols.christoffelSymbol {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (i j k : Fin n) : ℝ

theorem ChristoffelSymbols.secondPartialDeriv_symmetric {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (i j : Fin n) : secondPartialDeriv patch x i j = secondPartialDeriv patch x j i

noncomputable def partialDeriv {n : ℕ} (i : Fin n) (g : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) : ℝ

theorem ChristoffelFromMetric.firstFundamentalForm_symmetric {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (i j : Fin n) : firstFundamentalForm patch x i j = firstFundamentalForm patch x j i

theorem ChristoffelFromMetric.firstFundamentalForm_isHermitian {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) : (firstFundamentalForm patch x).IsHermitian

theorem ChristoffelFromMetric.firstFundamentalForm_inv_symmetric {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (i j : Fin n) : (firstFundamentalForm patch x)⁻¹ i j = (firstFundamentalForm patch x)⁻¹ j i

theorem ChristoffelFromMetric.metric_partialDeriv_eq {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (a b m : Fin n) : partialDeriv m (fun (y : Fin n → ℝ) => firstFundamentalForm patch y a b) x = ChristoffelSymbols.secondPartialDeriv patch x m a ⬝ᵥ patch.partialDeriv x b + patch.partialDeriv x a ⬝ᵥ ChristoffelSymbols.secondPartialDeriv patch x m b

theorem ChristoffelFromMetric.inner_secondPartial_eq_half_metric_derivs {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (i j l : Fin n) : ChristoffelSymbols.secondPartialDeriv patch x i j ⬝ᵥ patch.partialDeriv x l = 1 / 2 * (partialDeriv j (fun (y : Fin n → ℝ) => firstFundamentalForm patch y i l) x - partialDeriv l (fun (y : Fin n → ℝ) => firstFundamentalForm patch y i j) x + partialDeriv i (fun (y : Fin n → ℝ) => firstFundamentalForm patch y j l) x)

theorem ChristoffelFromMetric.christoffel_from_metric {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (i j l : Fin n) : ChristoffelSymbols.christoffelSymbol patch x i j l = 1 / 2 * ∑ k : Fin n, (firstFundamentalForm patch x)⁻¹ k l * (partialDeriv j (fun (y : Fin n → ℝ) => firstFundamentalForm patch y i k) x - partialDeriv k (fun (y : Fin n → ℝ) => firstFundamentalForm patch y i j) x + partialDeriv i (fun (y : Fin n → ℝ) => firstFundamentalForm patch y j k) x)

noncomputable def TensorDecomposition.tensorT {ι : Type u_1} {F : Type u_2} [Field F] (S : ι → ι → ι → F) (i j k : ι) : F

theorem TensorDecomposition.tensorT_symm_13 {ι : Type u_1} {F : Type u_2} [Field F] [CharZero F] (S : ι → ι → ι → F) (hS : ∀ (i j k : ι), S i j k = S j i k) (i j k : ι) : tensorT S i j k = tensorT S k j i

theorem TensorDecomposition.tensor_decomposition {ι : Type u_1} {F : Type u_2} [Field F] [CharZero F] (S : ι → ι → ι → F) (hS : ∀ (i j k : ι), S i j k = S j i k) (i j k : ι) : S i j k = tensorT S i j k + tensorT S j i k

theorem TensorDecomposition.exists_symmetric_tensor_decomposition {ι : Type u_1} {F : Type u_2} [Field F] [CharZero F] (S : ι → ι → ι → F) (hS : ∀ (i j k : ι), S i j k = S j i k) : ∃ (T : ι → ι → ι → F), (∀ (i j k : ι), T i j k = T k j i) ∧ ∀ (i j k : ι), S i j k = T i j k + T j i k

structure MovingFrame.IsMovingBasis {n : ℕ} (patch : HypersurfacePatch n) (X : (Fin n → ℝ) → Matrix (Fin n) (Fin n) ℝ) : Prop

• smooth : ContDiffOn ℝ ⊤ X patch.domain
• invertible (x : Fin n → ℝ) : x ∈ patch.domain → IsUnit (X x)

structure MovingFrame.IsMovingFrame {n : ℕ} (patch : HypersurfacePatch n) (X : (Fin n → ℝ) → Matrix (Fin n) (Fin n) ℝ) extends MovingFrame.IsMovingBasis patch X : Prop

• smooth : ContDiffOn ℝ ⊤ X patch.domain
• invertible (x : Fin n → ℝ) : x ∈ patch.domain → IsUnit (X x)
• orthonormal (x : Fin n → ℝ) : x ∈ patch.domain → (X x).transpose * firstFundamentalForm patch x * X x = 1

noncomputable def MovingFrame.christoffelMatrix {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (j : Fin n) : Matrix (Fin n) (Fin n) ℝ

noncomputable def MovingFrame.matrixPartialDeriv {n : ℕ} (X : (Fin n → ℝ) → Matrix (Fin n) (Fin n) ℝ) (x : Fin n → ℝ) (j : Fin n) : Matrix (Fin n) (Fin n) ℝ

noncomputable def MovingFrame.connectionMatrix {n : ℕ} (patch : HypersurfacePatch n) (X : (Fin n → ℝ) → Matrix (Fin n) (Fin n) ℝ) (x : Fin n → ℝ) (j : Fin n) : Matrix (Fin n) (Fin n) ℝ

noncomputable def MovingFrame.curvatureMatrix {n : ℕ} (patch : HypersurfacePatch n) (X : (Fin n → ℝ) → Matrix (Fin n) (Fin n) ℝ) (x : Fin n → ℝ) (k j : Fin n) : Matrix (Fin n) (Fin n) ℝ

noncomputable def MovingFrame.riemannCurvatureMatrix {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (k j : Fin n) : Matrix (Fin n) (Fin n) ℝ

theorem MovingFrame.connectionMatrix_fderiv_leibniz {n : ℕ} (patch : HypersurfacePatch n) (X : (Fin n → ℝ) → Matrix (Fin n) (Fin n) ℝ) (hX : IsMovingBasis patch X) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (k j : Fin n) : (fderiv ℝ (fun (y : Fin n → ℝ) => (X y)⁻¹ * matrixPartialDeriv X y j + (X y)⁻¹ * christoffelMatrix patch y j * X y) x) (Pi.single k 1) = -(X x)⁻¹ * matrixPartialDeriv X x k * (X x)⁻¹ * matrixPartialDeriv X x j + (fderiv ℝ (fun (y : Fin n → ℝ) => matrixPartialDeriv X y j) x) (Pi.single k 1) - (X x)⁻¹ * matrixPartialDeriv X x k * (X x)⁻¹ * christoffelMatrix patch x j * X x + (X x)⁻¹ * (fderiv ℝ (fun (y : Fin n → ℝ) => christoffelMatrix patch y j) x) (Pi.single k 1) * X x + (X x)⁻¹ * christoffelMatrix patch x j * matrixPartialDeriv X x k

theorem MovingFrame.matrixPartialDeriv_comm {n : ℕ} (X : (Fin n → ℝ) → Matrix (Fin n) (Fin n) ℝ) {s : Set (Fin n → ℝ)} (hs : IsOpen s) (hX_smooth : ContDiffOn ℝ ⊤ X s) (x : Fin n → ℝ) (hx : x ∈ s) (k j : Fin n) : (fderiv ℝ (fun (y : Fin n → ℝ) => matrixPartialDeriv X y j) x) (Pi.single k 1) = (fderiv ℝ (fun (y : Fin n → ℝ) => matrixPartialDeriv X y k) x) (Pi.single j 1)

theorem MovingFrame.curvatureMatrix_eq_conjugate {n : ℕ} (patch : HypersurfacePatch n) (X : (Fin n → ℝ) → Matrix (Fin n) (Fin n) ℝ) (hX : IsMovingBasis patch X) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (k j : Fin n) : curvatureMatrix patch X x k j = (X x)⁻¹ * riemannCurvatureMatrix patch x k j * X x

noncomputable def MovingFrame.metricPartialDeriv {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (j : Fin n) : Matrix (Fin n) (Fin n) ℝ

theorem MovingFrame.metricCompatibility_matrix {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (j : Fin n) : metricPartialDeriv patch x j = (christoffelMatrix patch x j).transpose * firstFundamentalForm patch x + firstFundamentalForm patch x * christoffelMatrix patch x j

theorem MovingFrame.fderiv_tripleProduct_matrix {n : ℕ} (patch : HypersurfacePatch n) (X : (Fin n → ℝ) → Matrix (Fin n) (Fin n) ℝ) (hF : IsMovingFrame patch X) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (j : Fin n) : (fderiv ℝ (fun (y : Fin n → ℝ) => (X y).transpose * firstFundamentalForm patch y * X y) x) (Pi.single j 1) = (matrixPartialDeriv X x j).transpose * firstFundamentalForm patch x * X x + (X x).transpose * metricPartialDeriv patch x j * X x + (X x).transpose * firstFundamentalForm patch x * matrixPartialDeriv X x j

theorem MovingFrame.connectionMatrix_skewSymmetric {n : ℕ} (patch : HypersurfacePatch n) (X : (Fin n → ℝ) → Matrix (Fin n) (Fin n) ℝ) (hF : IsMovingFrame patch X) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (j : Fin n) : (connectionMatrix patch X x j).transpose = -connectionMatrix patch X x j

theorem MovingFrame.skewSymm_commutator_01_eq_zero (A B : Matrix (Fin 2) (Fin 2) ℝ) (hA : A.transpose = -A) (hB : B.transpose = -B) : (A * B - B * A) 0 1 = 0

theorem MovingFrame.riemannCurvatureMatrix_eq_gaussCurvature_mul_det (patch : HypersurfacePatch 2) (x : Fin 2 → ℝ) (hx : x ∈ patch.domain) : riemannCurvatureMatrix patch x 1 0 0 1 = gaussCurvature patch x * (firstFundamentalForm patch x).det

theorem MovingFrame.riemannCurvatureMatrix_metric_skew (patch : HypersurfacePatch 2) (x : Fin 2 → ℝ) (hx : x ∈ patch.domain) (k j : Fin 2) : (firstFundamentalForm patch x * riemannCurvatureMatrix patch x k j).transpose = -(firstFundamentalForm patch x * riemannCurvatureMatrix patch x k j)

theorem MovingFrame.riemannCurvatureMatrix_GR_entry (patch : HypersurfacePatch 2) (x : Fin 2 → ℝ) (hx : x ∈ patch.domain) : (firstFundamentalForm patch x * riemannCurvatureMatrix patch x 1 0) 0 1 = riemannCurvatureMatrix patch x 1 0 0 1

theorem MovingFrame.conjScale_riemannCurvatureMatrix (patch : HypersurfacePatch 2) (X : (Fin 2 → ℝ) → Matrix (Fin 2) (Fin 2) ℝ) (hF : IsMovingFrame patch X) (x : Fin 2 → ℝ) (hx : x ∈ patch.domain) : ((X x)⁻¹ * riemannCurvatureMatrix patch x 1 0 * X x) 0 1 = riemannCurvatureMatrix patch x 1 0 0 1 * (X x).det

theorem MovingFrame.gaussCurvature_eq_curvatureMatrix_entry (patch : HypersurfacePatch 2) (X : (Fin 2 → ℝ) → Matrix (Fin 2) (Fin 2) ℝ) (hF : IsMovingFrame patch X) (x : Fin 2 → ℝ) (hx : x ∈ patch.domain) (hpos : 0 < (X x).det) : gaussCurvature patch x * √(firstFundamentalForm patch x).det = curvatureMatrix patch X x 1 0 0 1

def NormalCoordinates.transformedMetricLinear {n : ℕ} (G B : Matrix (Fin n) (Fin n) ℝ) : Matrix (Fin n) (Fin n) ℝ

theorem NormalCoordinates.exists_linear_change_identity_metric {n : ℕ} (G : Matrix (Fin n) (Fin n) ℝ) (hG : G.PosDef) : ∃ (B : Matrix (Fin n) (Fin n) ℝ), B.transpose = B ∧ IsUnit B.det ∧ transformedMetricLinear G B = 1

theorem NormalCoordinates.exists_reparam_identity_metric_at_point {n : ℕ} (patch : HypersurfacePatch n) (p : Fin n → ℝ) (_hp : p ∈ patch.domain) (hG : (firstFundamentalForm patch p).PosDef) : ∃ (B : Matrix (Fin n) (Fin n) ℝ), B.transpose = B ∧ IsUnit B.det ∧ transformedMetricLinear (firstFundamentalForm patch p) B = 1

theorem NormalCoordinates.exists_normal_coordinates {n : ℕ} (G : Matrix (Fin n) (Fin n) ℝ) (hG : G.PosDef) (S : Fin n → Fin n → Fin n → ℝ) (hS_symm : ∀ (i j k : Fin n), S i j k = S j i k) : ∃ (B : Matrix (Fin n) (Fin n) ℝ) (T : Fin n → Fin n → Fin n → ℝ), (B.transpose = B ∧ IsUnit B.det ∧ transformedMetricLinear G B = 1) ∧ (∀ (i j k : Fin n), T i j k = T k j i) ∧ ∀ (i j k : Fin n), S i j k = T i j k + T j i k

def NormalCoordinates.metricDerivAfterQuadraticChange {n : ℕ} (S T : Fin n → Fin n → Fin n → ℝ) (i j k : Fin n) : ℝ

theorem NormalCoordinates.metric_deriv_vanishes_of_decomposition {n : ℕ} (S T : Fin n → Fin n → Fin n → ℝ) (hDecomp : ∀ (i j k : Fin n), S i j k = T i j k + T j i k) (i j k : Fin n) : metricDerivAfterQuadraticChange S T i j k = 0

theorem NormalCoordinates.exists_normal_coordinates_vanishing_derivs_algebraic {n : ℕ} (G : Matrix (Fin n) (Fin n) ℝ) (hG : G.PosDef) (S : Fin n → Fin n → Fin n → ℝ) (hS_symm : ∀ (i j k : Fin n), S i j k = S j i k) : ∃ (B : Matrix (Fin n) (Fin n) ℝ) (T : Fin n → Fin n → Fin n → ℝ), (B.transpose = B ∧ IsUnit B.det ∧ transformedMetricLinear G B = 1) ∧ (∀ (i j k : Fin n), T i j k = T k j i) ∧ ∀ (i j k : Fin n), metricDerivAfterQuadraticChange S T i j k = 0

theorem NormalCoordinates.exists_normal_coordinates_vanishing_derivs {n : ℕ} (patch : HypersurfacePatch n) (p : Fin n → ℝ) (_hp : p ∈ patch.domain) (hG : (firstFundamentalForm patch p).PosDef) (hDiff : DifferentiableAt ℝ (firstFundamentalForm patch) p) : have S := fun (i j k : Fin n) => MovingFrame.metricPartialDeriv patch p k i j; ∃ (B : Matrix (Fin n) (Fin n) ℝ) (T : Fin n → Fin n → Fin n → ℝ), (B.transpose = B ∧ IsUnit B.det ∧ transformedMetricLinear (firstFundamentalForm patch p) B = 1) ∧ (∀ (i j k : Fin n), T i j k = T k j i) ∧ ∀ (i j k : Fin n), metricDerivAfterQuadraticChange S T i j k = 0

noncomputable def RiemannIntrinsic.riemannCurvature {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (i j k s : Fin n) : ℝ

theorem RiemannIntrinsic.fderiv_eq_of_eq_on_open {n : ℕ} {f g : (Fin n → ℝ) → ℝ} {s : Set (Fin n → ℝ)} (hs : IsOpen s) {x : Fin n → ℝ} (hx : x ∈ s) (hfg : ∀ y ∈ s, f y = g y) : fderiv ℝ f x = fderiv ℝ g x

theorem RiemannIntrinsic.partialDeriv_metric_eq {n : ℕ} (patch₁ patch₂ : HypersurfacePatch n) (_hdom : patch₁.domain = patch₂.domain) (hG : ∀ x ∈ patch₁.domain, firstFundamentalForm patch₁ x = firstFundamentalForm patch₂ x) (x : Fin n → ℝ) (hx : x ∈ patch₁.domain) (i j m : Fin n) : partialDeriv m (fun (y : Fin n → ℝ) => firstFundamentalForm patch₁ y i j) x = partialDeriv m (fun (y : Fin n → ℝ) => firstFundamentalForm patch₂ y i j) x

theorem RiemannIntrinsic.christoffelSymbol_eq_of_metric_eq {n : ℕ} (patch₁ patch₂ : HypersurfacePatch n) (hdom : patch₁.domain = patch₂.domain) (hG : ∀ x ∈ patch₁.domain, firstFundamentalForm patch₁ x = firstFundamentalForm patch₂ x) (x : Fin n → ℝ) (hx : x ∈ patch₁.domain) (i j l : Fin n) : ChristoffelSymbols.christoffelSymbol patch₁ x i j l = ChristoffelSymbols.christoffelSymbol patch₂ x i j l

theorem RiemannIntrinsic.christoffelMatrix_eq_of_metric_eq {n : ℕ} (patch₁ patch₂ : HypersurfacePatch n) (hdom : patch₁.domain = patch₂.domain) (hG : ∀ x ∈ patch₁.domain, firstFundamentalForm patch₁ x = firstFundamentalForm patch₂ x) (x : Fin n → ℝ) (hx : x ∈ patch₁.domain) (j : Fin n) : MovingFrame.christoffelMatrix patch₁ x j = MovingFrame.christoffelMatrix patch₂ x j

theorem RiemannIntrinsic.fderiv_christoffelMatrix_eq_of_metric_eq {n : ℕ} (patch₁ patch₂ : HypersurfacePatch n) (hdom : patch₁.domain = patch₂.domain) (hG : ∀ x ∈ patch₁.domain, firstFundamentalForm patch₁ x = firstFundamentalForm patch₂ x) (x : Fin n → ℝ) (hx : x ∈ patch₁.domain) (j k : Fin n) : (fderiv ℝ (fun (y : Fin n → ℝ) => MovingFrame.christoffelMatrix patch₁ y j) x) (Pi.single k 1) = (fderiv ℝ (fun (y : Fin n → ℝ) => MovingFrame.christoffelMatrix patch₂ y j) x) (Pi.single k 1)

theorem RiemannIntrinsic.generalized_theorema_egregium {n : ℕ} (patch₁ patch₂ : HypersurfacePatch n) (hdom : patch₁.domain = patch₂.domain) (hG : ∀ x ∈ patch₁.domain, firstFundamentalForm patch₁ x = firstFundamentalForm patch₂ x) (x : Fin n → ℝ) : x ∈ patch₁.domain → ∀ (i j k s : Fin n), riemannCurvature patch₁ x i j k s = riemannCurvature patch₂ x i j k s

noncomputable def GaussEquation.riemannCurvature {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (i j k s : Fin n) : ℝ

noncomputable def GaussEquation.thirdPartialDeriv {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (i j k : Fin n) : Fin (n + 1) → ℝ

noncomputable def GaussEquation.thirdDerivTangComp {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (i j k s : Fin n) : ℝ

theorem GaussEquation.thirdPartialDeriv_symm_jk {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (i j k : Fin n) : thirdPartialDeriv patch x i j k = thirdPartialDeriv patch x i k j

theorem GaussEquation.thirdDerivTangComp_symm_jk {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (i j k s : Fin n) : thirdDerivTangComp patch x i j k s = thirdDerivTangComp patch x i k j s

theorem GaussEquation.tangential_formula_eq {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (i j k s : Fin n) : thirdDerivTangComp patch x i j k s = partialDeriv k (fun (y : Fin n → ℝ) => ChristoffelSymbols.christoffelSymbol patch y i j s) x + ∑ t : Fin n, ChristoffelSymbols.christoffelSymbol patch x i j t * ChristoffelSymbols.christoffelSymbol patch x k t s - secondFundamentalForm patch x i j * shapeOperator patch x s k

theorem GaussEquation.tangential_component_third_deriv {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (i j k s : Fin n) : partialDeriv k (fun (y : Fin n → ℝ) => ChristoffelSymbols.christoffelSymbol patch y i j s) x + ∑ t : Fin n, ChristoffelSymbols.christoffelSymbol patch x i j t * ChristoffelSymbols.christoffelSymbol patch x k t s - secondFundamentalForm patch x i j * shapeOperator patch x s k = partialDeriv j (fun (y : Fin n → ℝ) => ChristoffelSymbols.christoffelSymbol patch y i k s) x + ∑ t : Fin n, ChristoffelSymbols.christoffelSymbol patch x i k t * ChristoffelSymbols.christoffelSymbol patch x j t s - secondFundamentalForm patch x i k * shapeOperator patch x s j

theorem GaussEquation.gauss_equation {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (i j k s : Fin n) : secondFundamentalForm patch x i j * shapeOperator patch x s k - secondFundamentalForm patch x i k * shapeOperator patch x s j = riemannCurvature patch x i j k s

noncomputable def IntrinsicCurvatures.exteriorPowerShapeOp {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (i j k s : Fin n) : ℝ

theorem IntrinsicCurvatures.principalCurvatureProducts_intrinsic {n : ℕ} (patch₁ patch₂ : HypersurfacePatch n) (hdom : patch₁.domain = patch₂.domain) (hG : ∀ x ∈ patch₁.domain, firstFundamentalForm patch₁ x = firstFundamentalForm patch₂ x) (x : Fin n → ℝ) : x ∈ patch₁.domain → ∀ (i j k s : Fin n), exteriorPowerShapeOp patch₁ x i j k s = exteriorPowerShapeOp patch₂ x i j k s

noncomputable def IntrinsicCurvatures.exteriorPowerShapeOpMatrix {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) : Matrix (Fin n × Fin n) (Fin n × Fin n) ℝ

theorem IntrinsicCurvatures.principalCurvatureProducts_matrix_intrinsic {n : ℕ} (patch₁ patch₂ : HypersurfacePatch n) (hdom : patch₁.domain = patch₂.domain) (hG : ∀ x ∈ patch₁.domain, firstFundamentalForm patch₁ x = firstFundamentalForm patch₂ x) (x : Fin n → ℝ) : x ∈ patch₁.domain → exteriorPowerShapeOpMatrix patch₁ x = exteriorPowerShapeOpMatrix patch₂ x

@[reducible, inline]

abbrev IntrinsicCurvatures.AntisymIndex (n : ℕ) : Type

noncomputable def IntrinsicCurvatures.exteriorPowerShapeOpMatrix_antisym {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) : Matrix (AntisymIndex n) (AntisymIndex n) ℝ

theorem IntrinsicCurvatures.compoundMatrix_diagonal_entries {n : ℕ} (D : Fin n → ℝ) (p q : AntisymIndex n) : Matrix.diagonal D (↑p).1 (↑q).1 * Matrix.diagonal D (↑p).2 (↑q).2 - Matrix.diagonal D (↑p).1 (↑q).2 * Matrix.diagonal D (↑p).2 (↑q).1 = if p = q then D (↑p).1 * D (↑p).2 else 0

theorem IntrinsicCurvatures.compoundMatrix_diagonal_eq {n : ℕ} (D : Fin n → ℝ) : (Matrix.of fun (p q : AntisymIndex n) => Matrix.diagonal D (↑p).1 (↑q).1 * Matrix.diagonal D (↑p).2 (↑q).2 - Matrix.diagonal D (↑p).1 (↑q).2 * Matrix.diagonal D (↑p).2 (↑q).1) = Matrix.diagonal fun (p : AntisymIndex n) => D (↑p).1 * D (↑p).2

theorem IntrinsicCurvatures.principalCurvatureProducts_antisym_intrinsic {n : ℕ} (patch₁ patch₂ : HypersurfacePatch n) (hdom : patch₁.domain = patch₂.domain) (hG : ∀ x ∈ patch₁.domain, firstFundamentalForm patch₁ x = firstFundamentalForm patch₂ x) (x : Fin n → ℝ) : x ∈ patch₁.domain → exteriorPowerShapeOpMatrix_antisym patch₁ x = exteriorPowerShapeOpMatrix_antisym patch₂ x

theorem IntrinsicCurvatures.principalCurvatureProducts_antisym_charpoly_intrinsic {n : ℕ} (patch₁ patch₂ : HypersurfacePatch n) (hdom : patch₁.domain = patch₂.domain) (hG : ∀ x ∈ patch₁.domain, firstFundamentalForm patch₁ x = firstFundamentalForm patch₂ x) (x : Fin n → ℝ) : x ∈ patch₁.domain → (exteriorPowerShapeOpMatrix_antisym patch₁ x).charpoly = (exteriorPowerShapeOpMatrix_antisym patch₂ x).charpoly

theorem IntrinsicCurvatures.scalarCurvature_intrinsic {n : ℕ} (patch₁ patch₂ : HypersurfacePatch n) (hdom : patch₁.domain = patch₂.domain) (hG : ∀ x ∈ patch₁.domain, firstFundamentalForm patch₁ x = firstFundamentalForm patch₂ x) (x : Fin n → ℝ) : x ∈ patch₁.domain → scalarCurvature patch₁ x = scalarCurvature patch₂ x

theorem IntrinsicCurvatures.det_pow_eq_of_minors_eq {n : ℕ} (L₁ L₂ : Matrix (Fin n) (Fin n) ℝ) (hMinors : ∀ (i j k s : Fin n), L₁ i k * L₁ j s - L₁ i s * L₁ j k = L₂ i k * L₂ j s - L₂ i s * L₂ j k) : L₁.det ^ (n - 1) = L₂.det ^ (n - 1)

theorem IntrinsicCurvatures.gaussCurvature_pow_intrinsic {n : ℕ} (patch₁ patch₂ : HypersurfacePatch n) (hdom : patch₁.domain = patch₂.domain) (hG : ∀ x ∈ patch₁.domain, firstFundamentalForm patch₁ x = firstFundamentalForm patch₂ x) (x : Fin n → ℝ) : x ∈ patch₁.domain → gaussCurvature patch₁ x ^ (n - 1) = gaussCurvature patch₂ x ^ (n - 1)

theorem IntrinsicCurvatures.gaussCurvature_intrinsic_even {n : ℕ} (hn : Even n) (hn_pos : 0 < n) (patch₁ patch₂ : HypersurfacePatch n) (hdom : patch₁.domain = patch₂.domain) (hG : ∀ x ∈ patch₁.domain, firstFundamentalForm patch₁ x = firstFundamentalForm patch₂ x) (x : Fin n → ℝ) : x ∈ patch₁.domain → gaussCurvature patch₁ x = gaussCurvature patch₂ x

theorem IntrinsicCurvatures.absGaussCurvature_intrinsic_odd {n : ℕ} (hn : Odd n) (hn_ge : 3 ≤ n) (patch₁ patch₂ : HypersurfacePatch n) (hdom : patch₁.domain = patch₂.domain) (hG : ∀ x ∈ patch₁.domain, firstFundamentalForm patch₁ x = firstFundamentalForm patch₂ x) (x : Fin n → ℝ) : x ∈ patch₁.domain → |gaussCurvature patch₁ x| = |gaussCurvature patch₂ x|

theorem IntrinsicCurvatures.scalarCurvature_gaussCurvature_intrinsic : (∀ {n : ℕ} (patch₁ patch₂ : HypersurfacePatch n), patch₁.domain = patch₂.domain → (∀ x ∈ patch₁.domain, firstFundamentalForm patch₁ x = firstFundamentalForm patch₂ x) → ∀ x ∈ patch₁.domain, scalarCurvature patch₁ x = scalarCurvature patch₂ x) ∧ (∀ {n : ℕ} (patch₁ patch₂ : HypersurfacePatch n), patch₁.domain = patch₂.domain → (∀ x ∈ patch₁.domain, firstFundamentalForm patch₁ x = firstFundamentalForm patch₂ x) → ∀ x ∈ patch₁.domain, gaussCurvature patch₁ x ^ (n - 1) = gaussCurvature patch₂ x ^ (n - 1)) ∧ (∀ {n : ℕ}, Even n → 0 < n → ∀ (patch₁ patch₂ : HypersurfacePatch n), patch₁.domain = patch₂.domain → (∀ x ∈ patch₁.domain, firstFundamentalForm patch₁ x = firstFundamentalForm patch₂ x) → ∀ x ∈ patch₁.domain, gaussCurvature patch₁ x = gaussCurvature patch₂ x) ∧ ∀ {n : ℕ}, Odd n → 3 ≤ n → ∀ (patch₁ patch₂ : HypersurfacePatch n), patch₁.domain = patch₂.domain → (∀ x ∈ patch₁.domain, firstFundamentalForm patch₁ x = firstFundamentalForm patch₂ x) → ∀ x ∈ patch₁.domain, |gaussCurvature patch₁ x| = |gaussCurvature patch₂ x|

theorem RigidityRank3.rank3_products_determine_sign (a b c a' b' c' : ℝ) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hab : a * b = a' * b') (hac : a * c = a' * c') (hbc : b * c = b' * c') : a' = a ∧ b' = b ∧ c' = c ∨ a' = -a ∧ b' = -b ∧ c' = -c

theorem RigidityRank3.exteriorPower_rank3_implies_H_eq_or_neg {n : ℕ} (patch₁ patch₂ : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch₁.domain) (hdomain : patch₁.domain = patch₂.domain) (hG_eq : firstFundamentalForm patch₁ x = firstFundamentalForm patch₂ x) (hext : ∀ (i j k s : Fin n), IntrinsicCurvatures.exteriorPowerShapeOp patch₁ x i j k s = IntrinsicCurvatures.exteriorPowerShapeOp patch₂ x i j k s) (hrank : 3 ≤ (secondFundamentalForm patch₁ x).rank) : secondFundamentalForm patch₁ x = secondFundamentalForm patch₂ x ∨ secondFundamentalForm patch₁ x = -secondFundamentalForm patch₂ x

theorem RigidityRank3.secondFF_sign_constant_on_connected {n : ℕ} (patch₁ patch₂ : HypersurfacePatch n) (hconn : IsConnected patch₁.domain) (hrank : ∀ x ∈ patch₁.domain, 3 ≤ (secondFundamentalForm patch₁ x).rank) (h_pw : ∀ x ∈ patch₁.domain, secondFundamentalForm patch₁ x = secondFundamentalForm patch₂ x ∨ secondFundamentalForm patch₁ x = -secondFundamentalForm patch₂ x) (x₁ : Fin n → ℝ) (hx₁ : x₁ ∈ patch₁.domain) (hx₁_neg : secondFundamentalForm patch₁ x₁ = -secondFundamentalForm patch₂ x₁) (x₂ : Fin n → ℝ) (hx₂ : x₂ ∈ patch₁.domain) (hx₂_pos : secondFundamentalForm patch₁ x₂ = secondFundamentalForm patch₂ x₂) : False

theorem RigidityRank3.secondFundamentalForm_eq_or_neg {n : ℕ} (patch₁ patch₂ : HypersurfacePatch n) (hconn : IsConnected patch₁.domain) (hdomain : patch₁.domain = patch₂.domain) (hG : ∀ x ∈ patch₁.domain, firstFundamentalForm patch₁ x = firstFundamentalForm patch₂ x) (hrank : ∀ x ∈ patch₁.domain, 3 ≤ (secondFundamentalForm patch₁ x).rank) : (∀ x ∈ patch₁.domain, secondFundamentalForm patch₁ x = secondFundamentalForm patch₂ x) ∨ ∀ x ∈ patch₁.domain, secondFundamentalForm patch₁ x = -secondFundamentalForm patch₂ x

theorem RigidityRank3.rigidity_theorem_neg_H {n : ℕ} (patch₁ patch₂ : HypersurfacePatch n) (hconn : IsConnected patch₁.domain) (hdomain : patch₁.domain = patch₂.domain) (hG : ∀ x ∈ patch₁.domain, firstFundamentalForm patch₁ x = firstFundamentalForm patch₂ x) (hH : ∀ x ∈ patch₁.domain, secondFundamentalForm patch₁ x = -secondFundamentalForm patch₂ x) : ∃ (A : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ) (b : Fin (n + 1) → ℝ), A ∈ Matrix.orthogonalGroup (Fin (n + 1)) ℝ ∧ ∀ x ∈ patch₁.domain, patch₂.f x = A.mulVec (patch₁.f x) + b

theorem RigidityRank3.rigidity_of_rank_geq_three {n : ℕ} (patch₁ patch₂ : HypersurfacePatch n) (hconn : IsConnected patch₁.domain) (hdomain : patch₁.domain = patch₂.domain) (hG : ∀ x ∈ patch₁.domain, firstFundamentalForm patch₁ x = firstFundamentalForm patch₂ x) (hrank : ∀ x ∈ patch₁.domain, 3 ≤ (secondFundamentalForm patch₁ x).rank) : ∃ (A : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ) (c : Fin (n + 1) → ℝ), A ∈ Matrix.orthogonalGroup (Fin (n + 1)) ℝ ∧ ∀ x ∈ patch₁.domain, patch₂.f x = A.mulVec (patch₁.f x) + c

noncomputable def TheoremaEgregium.riemannCurvature (patch : HypersurfacePatch 2) (x : Fin 2 → ℝ) (i j k s : Fin 2) : ℝ

theorem TheoremaEgregium.theorema_egregium (patch : HypersurfacePatch 2) (x : Fin 2 → ℝ) (hx : x ∈ patch.domain) : gaussCurvature patch x = (∑ u : Fin 2, firstFundamentalForm patch x 1 u * riemannCurvature patch x 0 0 1 u) / (firstFundamentalForm patch x).det

theorem GaussBonnetTorus.gauss_bonnet_torus_integration_step (patch : HypersurfacePatch 2) (T₁ T₂ : ℝ) (α₁ α₂ : ℝ → ℝ → ℝ) (hProp18_4 : ∀ (x₁ x₂ : ℝ), gaussCurvature patch ![x₁, x₂] * √(firstFundamentalForm patch ![x₁, x₂]).det = deriv (α₁ x₁) x₂ - deriv (fun (t : ℝ) => α₂ t x₂) x₁) (hα₁_per : ∀ (x₁ : ℝ), α₁ x₁ T₂ = α₁ x₁ 0) (hα₂_per : ∀ (x₂ : ℝ), α₂ T₁ x₂ = α₂ 0 x₂) (hα₁_deriv : ∀ (x₁ x₂ : ℝ), x₂ ∈ Set.uIcc 0 T₂ → HasDerivAt (α₁ x₁) (deriv (α₁ x₁) x₂) x₂) (hα₂_deriv : ∀ (x₂ x₁ : ℝ), x₁ ∈ Set.uIcc 0 T₁ → HasDerivAt (fun (t : ℝ) => α₂ t x₂) (deriv (fun (t : ℝ) => α₂ t x₂) x₁) x₁) (hα₁_int : ∀ (x₁ : ℝ), IntervalIntegrable (deriv (α₁ x₁)) MeasureTheory.volume 0 T₂) (hα₂_int : ∀ (x₂ : ℝ), IntervalIntegrable (deriv fun (t : ℝ) => α₂ t x₂) MeasureTheory.volume 0 T₁) (hFubini : ∫ (x₁ : ℝ) in 0..T₁, ∫ (x₂ : ℝ) in 0..T₂, deriv (fun (t : ℝ) => α₂ t x₂) x₁ = ∫ (x₂ : ℝ) in 0..T₂, ∫ (x₁ : ℝ) in 0..T₁, deriv (fun (t : ℝ) => α₂ t x₂) x₁) (h_sub_int : ∀ (x₁ : ℝ), IntervalIntegrable (fun (x₂ : ℝ) => deriv (fun (t : ℝ) => α₂ t x₂) x₁) MeasureTheory.volume 0 T₂) : ∫ (x₁ : ℝ) in 0..T₁, ∫ (x₂ : ℝ) in 0..T₂, gaussCurvature patch ![x₁, x₂] * √(firstFundamentalForm patch ![x₁, x₂]).det = 0

theorem GaussBonnetTorus.exists_periodic_orthonormal_frame (patch : HypersurfacePatch 2) (T₁ T₂ : ℝ) (hT₁ : T₁ > 0) (hT₂ : T₂ > 0) (hper₁ : ∀ (x : Fin 2 → ℝ), patch.f ![x 0 + T₁, x 1] = patch.f x) (hper₂ : ∀ (x : Fin 2 → ℝ), patch.f ![x 0, x 1 + T₂] = patch.f x) : ∃ (X : (Fin 2 → ℝ) → Matrix (Fin 2) (Fin 2) ℝ), MovingFrame.IsMovingFrame patch X ∧ (∀ (x : Fin 2 → ℝ), 0 < (X x).det) ∧ (∀ (x : Fin 2 → ℝ), X ![x 0 + T₁, x 1] = X x) ∧ ∀ (x : Fin 2 → ℝ), X ![x 0, x 1 + T₂] = X x

theorem GaussBonnetTorus.connectionMatrix_periodic (patch : HypersurfacePatch 2) (X : (Fin 2 → ℝ) → Matrix (Fin 2) (Fin 2) ℝ) (T₁ T₂ : ℝ) (hper₁ : ∀ (x : Fin 2 → ℝ), patch.f ![x 0 + T₁, x 1] = patch.f x) (hper₂ : ∀ (x : Fin 2 → ℝ), patch.f ![x 0, x 1 + T₂] = patch.f x) (hXper₁ : ∀ (x : Fin 2 → ℝ), X ![x 0 + T₁, x 1] = X x) (hXper₂ : ∀ (x : Fin 2 → ℝ), X ![x 0, x 1 + T₂] = X x) : (∀ (x : Fin 2 → ℝ) (j : Fin 2), MovingFrame.connectionMatrix patch X ![x 0 + T₁, x 1] j = MovingFrame.connectionMatrix patch X x j) ∧ ∀ (x : Fin 2 → ℝ) (j : Fin 2), MovingFrame.connectionMatrix patch X ![x 0, x 1 + T₂] j = MovingFrame.connectionMatrix patch X x j

theorem GaussBonnetTorus.connection_form_curvature_identity (patch : HypersurfacePatch 2) (X : (Fin 2 → ℝ) → Matrix (Fin 2) (Fin 2) ℝ) (hF : MovingFrame.IsMovingFrame patch X) (hpos : ∀ (x : Fin 2 → ℝ), 0 < (X x).det) : have α₁ := fun (x₁ x₂ : ℝ) => MovingFrame.connectionMatrix patch X ![x₁, x₂] 0 0 1; have α₂ := fun (x₁ x₂ : ℝ) => MovingFrame.connectionMatrix patch X ![x₁, x₂] 1 0 1; ∀ (x₁ x₂ : ℝ), gaussCurvature patch ![x₁, x₂] * √(firstFundamentalForm patch ![x₁, x₂]).det = deriv (α₁ x₁) x₂ - deriv (fun (t : ℝ) => α₂ t x₂) x₁

theorem GaussBonnetTorus.connection_form_regularity (patch : HypersurfacePatch 2) (X : (Fin 2 → ℝ) → Matrix (Fin 2) (Fin 2) ℝ) (hF : MovingFrame.IsMovingFrame patch X) (T₁ T₂ : ℝ) (hT₁ : T₁ > 0) (hT₂ : T₂ > 0) : have α₁ := fun (x₁ x₂ : ℝ) => MovingFrame.connectionMatrix patch X ![x₁, x₂] 0 0 1; have α₂ := fun (x₁ x₂ : ℝ) => MovingFrame.connectionMatrix patch X ![x₁, x₂] 1 0 1; (∀ (x₁ x₂ : ℝ), x₂ ∈ Set.uIcc 0 T₂ → HasDerivAt (α₁ x₁) (deriv (α₁ x₁) x₂) x₂) ∧ (∀ (x₂ x₁ : ℝ), x₁ ∈ Set.uIcc 0 T₁ → HasDerivAt (fun (t : ℝ) => α₂ t x₂) (deriv (fun (t : ℝ) => α₂ t x₂) x₁) x₁) ∧ (∀ (x₁ : ℝ), IntervalIntegrable (deriv (α₁ x₁)) MeasureTheory.volume 0 T₂) ∧ (∀ (x₂ : ℝ), IntervalIntegrable (deriv fun (t : ℝ) => α₂ t x₂) MeasureTheory.volume 0 T₁) ∧ ∫ (x₁ : ℝ) in 0..T₁, ∫ (x₂ : ℝ) in 0..T₂, deriv (fun (t : ℝ) => α₂ t x₂) x₁ = ∫ (x₂ : ℝ) in 0..T₂, ∫ (x₁ : ℝ) in 0..T₁, deriv (fun (t : ℝ) => α₂ t x₂) x₁ ∧ ∀ (x₁ : ℝ), IntervalIntegrable (fun (x₂ : ℝ) => deriv (fun (t : ℝ) => α₂ t x₂) x₁) MeasureTheory.volume 0 T₂

theorem GaussBonnetTorus.periodic_connection_forms_exist (patch : HypersurfacePatch 2) (T₁ T₂ : ℝ) (hT₁ : T₁ > 0) (hT₂ : T₂ > 0) (hper₁ : ∀ (x : Fin 2 → ℝ), patch.f ![x 0 + T₁, x 1] = patch.f x) (hper₂ : ∀ (x : Fin 2 → ℝ), patch.f ![x 0, x 1 + T₂] = patch.f x) : ∃ (α₁ : ℝ → ℝ → ℝ) (α₂ : ℝ → ℝ → ℝ), (∀ (x₁ x₂ : ℝ), gaussCurvature patch ![x₁, x₂] * √(firstFundamentalForm patch ![x₁, x₂]).det = deriv (α₁ x₁) x₂ - deriv (fun (t : ℝ) => α₂ t x₂) x₁) ∧ (∀ (x₁ : ℝ), α₁ x₁ T₂ = α₁ x₁ 0) ∧ (∀ (x₂ : ℝ), α₂ T₁ x₂ = α₂ 0 x₂) ∧ (∀ (x₁ x₂ : ℝ), x₂ ∈ Set.uIcc 0 T₂ → HasDerivAt (α₁ x₁) (deriv (α₁ x₁) x₂) x₂) ∧ (∀ (x₂ x₁ : ℝ), x₁ ∈ Set.uIcc 0 T₁ → HasDerivAt (fun (t : ℝ) => α₂ t x₂) (deriv (fun (t : ℝ) => α₂ t x₂) x₁) x₁) ∧ (∀ (x₁ : ℝ), IntervalIntegrable (deriv (α₁ x₁)) MeasureTheory.volume 0 T₂) ∧ (∀ (x₂ : ℝ), IntervalIntegrable (deriv fun (t : ℝ) => α₂ t x₂) MeasureTheory.volume 0 T₁) ∧ ∫ (x₁ : ℝ) in 0..T₁, ∫ (x₂ : ℝ) in 0..T₂, deriv (fun (t : ℝ) => α₂ t x₂) x₁ = ∫ (x₂ : ℝ) in 0..T₂, ∫ (x₁ : ℝ) in 0..T₁, deriv (fun (t : ℝ) => α₂ t x₂) x₁ ∧ ∀ (x₁ : ℝ), IntervalIntegrable (fun (x₂ : ℝ) => deriv (fun (t : ℝ) => α₂ t x₂) x₁) MeasureTheory.volume 0 T₂

theorem GaussBonnetTorus.gauss_bonnet_torus (patch : HypersurfacePatch 2) (T₁ T₂ : ℝ) (hT₁ : T₁ > 0) (hT₂ : T₂ > 0) (hper₁ : ∀ (x : Fin 2 → ℝ), patch.f ![x 0 + T₁, x 1] = patch.f x) (hper₂ : ∀ (x : Fin 2 → ℝ), patch.f ![x 0, x 1 + T₂] = patch.f x) : ∫ (x₁ : ℝ) in 0..T₁, ∫ (x₂ : ℝ) in 0..T₂, gaussCurvature patch ![x₁, x₂] * √(firstFundamentalForm patch ![x₁, x₂]).det = 0

theorem GaussBonnetTorus.interval_integral_nonpos_eq_zero_imp (patch : HypersurfacePatch 2) (T₁ T₂ : ℝ) (hT₁ : T₁ > 0) (hT₂ : T₂ > 0) (hTotal : ∫ (x₁ : ℝ) in 0..T₁, ∫ (x₂ : ℝ) in 0..T₂, gaussCurvature patch ![x₁, x₂] * √(firstFundamentalForm patch ![x₁, x₂]).det = 0) (hNonpos : ∀ x ∈ patch.domain, gaussCurvature patch x ≤ 0) (x : Fin 2 → ℝ) : x ∈ patch.domain → gaussCurvature patch x = 0

theorem GaussBonnetTorus.interval_integral_nonneg_eq_zero_imp (patch : HypersurfacePatch 2) (T₁ T₂ : ℝ) (hT₁ : T₁ > 0) (hT₂ : T₂ > 0) (hTotal : ∫ (x₁ : ℝ) in 0..T₁, ∫ (x₂ : ℝ) in 0..T₂, gaussCurvature patch ![x₁, x₂] * √(firstFundamentalForm patch ![x₁, x₂]).det = 0) (hNonneg : ∀ x ∈ patch.domain, gaussCurvature patch x ≥ 0) (x : Fin 2 → ℝ) : x ∈ patch.domain → gaussCurvature patch x = 0

theorem GaussBonnetTorus.flat_torus_curvature_nonvanishing (patch : HypersurfacePatch 2) (T₁ T₂ : ℝ) (hT₁ : T₁ > 0) (hT₂ : T₂ > 0) (hper₁ : ∀ (x : Fin 2 → ℝ), patch.f ![x 0 + T₁, x 1] = patch.f x) (hper₂ : ∀ (x : Fin 2 → ℝ), patch.f ![x 0, x 1 + T₂] = patch.f x) : ∃ x ∈ patch.domain, gaussCurvature patch x ≠ 0

theorem GaussBonnetTorus.torus_curvature_sign_change (patch : HypersurfacePatch 2) (T₁ T₂ : ℝ) (hT₁ : T₁ > 0) (hT₂ : T₂ > 0) (hper₁ : ∀ (x : Fin 2 → ℝ), patch.f ![x 0 + T₁, x 1] = patch.f x) (hper₂ : ∀ (x : Fin 2 → ℝ), patch.f ![x 0, x 1 + T₂] = patch.f x) : (∃ x ∈ patch.domain, gaussCurvature patch x > 0) ∧ ∃ x ∈ patch.domain, gaussCurvature patch x < 0

structure AbstractRiemannianMetric.RiemannianMetric (n : ℕ) : Type

• domain : Set (Fin n → ℝ)
• domain_open : IsOpen self.domain
• domain_nonempty : self.domain.Nonempty
• G : (Fin n → ℝ) → Matrix (Fin n) (Fin n) ℝ
• smooth : ContDiffOn ℝ ⊤ self.G self.domain
• symmetric (x : Fin n → ℝ) : x ∈ self.domain → (self.G x).transpose = self.G x
• posDef (x : Fin n → ℝ) : x ∈ self.domain → (self.G x).PosDef

structure AbstractGaussBonnet.RiemannianMetric2D : Type

• G : (Fin 2 → ℝ) → Matrix (Fin 2) (Fin 2) ℝ
• smooth : ContDiff ℝ ⊤ self.G
• symmetric (x : Fin 2 → ℝ) : (self.G x).transpose = self.G x
• posDef (x : Fin 2 → ℝ) : (self.G x).PosDef

noncomputable def AbstractGaussBonnet.scalarPartialDeriv (i : Fin 2) (f : (Fin 2 → ℝ) → ℝ) (x : Fin 2 → ℝ) : ℝ

noncomputable def AbstractGaussBonnet.abstractChristoffel (g : RiemannianMetric2D) (x : Fin 2 → ℝ) (i j k : Fin 2) : ℝ

noncomputable def AbstractGaussBonnet.abstractGaussCurvature (g : RiemannianMetric2D) (x : Fin 2 → ℝ) : ℝ

def AbstractGaussBonnet.IsDoublyPeriodic (g : RiemannianMetric2D) (T₁ T₂ : ℝ) : Prop

noncomputable def AbstractGaussBonnet.loweredChristoffel (g : RiemannianMetric2D) (i j k : Fin 2) (x : Fin 2 → ℝ) : ℝ

noncomputable def AbstractGaussBonnet.connectionFormF₁ (g : RiemannianMetric2D) (x : Fin 2 → ℝ) : ℝ

noncomputable def AbstractGaussBonnet.connectionFormF₂ (g : RiemannianMetric2D) (x : Fin 2 → ℝ) : ℝ

theorem AbstractGaussBonnet.gEntry_smooth (g : RiemannianMetric2D) (i j : Fin 2) : ContDiff ℝ ⊤ fun (x : Fin 2 → ℝ) => g.G x i j

theorem AbstractGaussBonnet.scalarPartialDeriv_smooth (g : RiemannianMetric2D) (i j k : Fin 2) : ContDiff ℝ ⊤ fun (x : Fin 2 → ℝ) => scalarPartialDeriv k (fun (y : Fin 2 → ℝ) => g.G y i j) x

theorem AbstractGaussBonnet.sqrtDetG_smooth (g : RiemannianMetric2D) : ContDiff ℝ ⊤ fun (x : Fin 2 → ℝ) => √(g.G x).det

theorem AbstractGaussBonnet.sqrtDetG_ne_zero (g : RiemannianMetric2D) (x : Fin 2 → ℝ) : √(g.G x).det ≠ 0

theorem AbstractGaussBonnet.connectionFormF₁_smooth (g : RiemannianMetric2D) : ContDiff ℝ ⊤ (connectionFormF₁ g)

theorem AbstractGaussBonnet.connectionFormF₂_smooth (g : RiemannianMetric2D) : ContDiff ℝ ⊤ (connectionFormF₂ g)

theorem AbstractGaussBonnet.fderiv_periodic {f : (Fin 2 → ℝ) → ℝ} (hf : ContDiff ℝ ⊤ f) {v : Fin 2 → ℝ} (hper : ∀ (z : Fin 2 → ℝ), f (z + v) = f z) (x : Fin 2 → ℝ) : fderiv ℝ f (x + v) = fderiv ℝ f x

theorem AbstractGaussBonnet.connectionForm_periodic_aux (g : RiemannianMetric2D) (v : Fin 2 → ℝ) (hGper : ∀ (z : Fin 2 → ℝ), g.G (z + v) = g.G z) (i j k : Fin 2) (x : Fin 2 → ℝ) : loweredChristoffel g i j k (x + v) = loweredChristoffel g i j k x

theorem AbstractGaussBonnet.connectionFormF₁_periodic (g : RiemannianMetric2D) (v : Fin 2 → ℝ) (hGper : ∀ (z : Fin 2 → ℝ), g.G (z + v) = g.G z) (x : Fin 2 → ℝ) : connectionFormF₁ g (x + v) = connectionFormF₁ g x

theorem AbstractGaussBonnet.connectionFormF₂_periodic (g : RiemannianMetric2D) (v : Fin 2 → ℝ) (hGper : ∀ (z : Fin 2 → ℝ), g.G (z + v) = g.G z) (x : Fin 2 → ℝ) : connectionFormF₂ g (x + v) = connectionFormF₂ g x

theorem AbstractGaussBonnet.connectionFormF₁_periodic_x0 (g : RiemannianMetric2D) (T₁ T₂ : ℝ) (hper : IsDoublyPeriodic g T₁ T₂) (x₁ x₂ : ℝ) : connectionFormF₁ g ![x₁ + T₁, x₂] = connectionFormF₁ g ![x₁, x₂]

theorem AbstractGaussBonnet.connectionFormF₁_periodic_x1 (g : RiemannianMetric2D) (T₁ T₂ : ℝ) (hper : IsDoublyPeriodic g T₁ T₂) (x₁ x₂ : ℝ) : connectionFormF₁ g ![x₁, x₂ + T₂] = connectionFormF₁ g ![x₁, x₂]

theorem AbstractGaussBonnet.connectionFormF₂_periodic_x0 (g : RiemannianMetric2D) (T₁ T₂ : ℝ) (hper : IsDoublyPeriodic g T₁ T₂) (x₁ x₂ : ℝ) : connectionFormF₂ g ![x₁ + T₁, x₂] = connectionFormF₂ g ![x₁, x₂]

theorem AbstractGaussBonnet.connectionFormF₂_periodic_x1 (g : RiemannianMetric2D) (T₁ T₂ : ℝ) (hper : IsDoublyPeriodic g T₁ T₂) (x₁ x₂ : ℝ) : connectionFormF₂ g ![x₁, x₂ + T₂] = connectionFormF₂ g ![x₁, x₂]

theorem AbstractGaussBonnet.connectionForm_divergence_identity (g : RiemannianMetric2D) (x : Fin 2 → ℝ) : abstractGaussCurvature g x * √(g.G x).det = scalarPartialDeriv 0 (connectionFormF₁ g) x + scalarPartialDeriv 1 (connectionFormF₂ g) x

theorem AbstractGaussBonnet.curvature_density_divergence_form (g : RiemannianMetric2D) (T₁ T₂ : ℝ) (hT₁ : T₁ > 0) (hT₂ : T₂ > 0) (hper : IsDoublyPeriodic g T₁ T₂) : ∃ (F₁ : (Fin 2 → ℝ) → ℝ) (F₂ : (Fin 2 → ℝ) → ℝ), ContDiff ℝ ⊤ F₁ ∧ ContDiff ℝ ⊤ F₂ ∧ (∀ (x₁ x₂ : ℝ), F₁ ![x₁ + T₁, x₂] = F₁ ![x₁, x₂]) ∧ (∀ (x₁ x₂ : ℝ), F₁ ![x₁, x₂ + T₂] = F₁ ![x₁, x₂]) ∧ (∀ (x₁ x₂ : ℝ), F₂ ![x₁ + T₁, x₂] = F₂ ![x₁, x₂]) ∧ (∀ (x₁ x₂ : ℝ), F₂ ![x₁, x₂ + T₂] = F₂ ![x₁, x₂]) ∧ ∀ (x : Fin 2 → ℝ), abstractGaussCurvature g x * √(g.G x).det = scalarPartialDeriv 0 F₁ x + scalarPartialDeriv 1 F₂ x

theorem AbstractGaussBonnet.integral_divergence_periodic_rectangle (F₁ F₂ : (Fin 2 → ℝ) → ℝ) (T₁ T₂ : ℝ) (hT₁ : T₁ > 0) (hT₂ : T₂ > 0) (hF₁_smooth : ContDiff ℝ ⊤ F₁) (hF₂_smooth : ContDiff ℝ ⊤ F₂) (hF₁_per1 : ∀ (x₁ x₂ : ℝ), F₁ ![x₁ + T₁, x₂] = F₁ ![x₁, x₂]) (hF₁_per2 : ∀ (x₁ x₂ : ℝ), F₁ ![x₁, x₂ + T₂] = F₁ ![x₁, x₂]) (hF₂_per1 : ∀ (x₁ x₂ : ℝ), F₂ ![x₁ + T₁, x₂] = F₂ ![x₁, x₂]) (hF₂_per2 : ∀ (x₁ x₂ : ℝ), F₂ ![x₁, x₂ + T₂] = F₂ ![x₁, x₂]) : ∫ (x₁ : ℝ) in 0..T₁, ∫ (x₂ : ℝ) in 0..T₂, scalarPartialDeriv 0 F₁ ![x₁, x₂] + scalarPartialDeriv 1 F₂ ![x₁, x₂] = 0

theorem AbstractGaussBonnet.gauss_bonnet_doubly_periodic_abstract (g : RiemannianMetric2D) (T₁ T₂ : ℝ) (hT₁ : T₁ > 0) (hT₂ : T₂ > 0) (hper : IsDoublyPeriodic g T₁ T₂) : ∫ (x₁ : ℝ) in 0..T₁, ∫ (x₂ : ℝ) in 0..T₂, abstractGaussCurvature g ![x₁, x₂] * √(g.G ![x₁, x₂]).det = 0