A determinant-one three-dimensional matrix has a quadratic inverse. This realizes the cofactor as an actual bounded bilinear map; its estimates therefore require no derivatives or norm bounds for a separately given inverse.

@[reducible, inline]

abbrev EulerPacketCofactor.EndSpace : Type

End space: an abbreviation for Space →L[ℝ] Space.

Equations

• EulerPacketCofactor.EndSpace = (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

@[instance_reducible]

noncomputable def EulerPacketCofactor.instPacketCofactorOperator1 : NormedAddCommGroup EndSpace

Cache the standard NormedAddCommGroup EndSpace instance to shorten typeclass synthesis.

Equations

• EulerPacketCofactor.instPacketCofactorOperator1 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCofactor.instPacketCofactorOperator2 : NormedSpace ℝ EndSpace

Cache the standard NormedSpace ℝ EndSpace instance to shorten typeclass synthesis.

Equations

• EulerPacketCofactor.instPacketCofactorOperator2 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCofactor.instPacketCofactorOperator3 : NormedAddCommGroup (EndSpace →L[ℝ] EndSpace)

Cache the standard NormedAddCommGroup (EndSpace →L[ℝ] EndSpace) instance to shorten typeclass synthesis.

Equations

• EulerPacketCofactor.instPacketCofactorOperator3 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCofactor.instPacketCofactorOperator4 : NormedSpace ℝ (EndSpace →L[ℝ] EndSpace)

Cache the standard NormedSpace ℝ (EndSpace →L[ℝ] EndSpace) instance to shorten typeclass synthesis.

Equations

• EulerPacketCofactor.instPacketCofactorOperator4 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCofactor.instPacketCofactorOperator5 : NormedAddCommGroup (EndSpace →L[ℝ] EndSpace →L[ℝ] EndSpace)

Cache the standard NormedAddCommGroup (EndSpace →L[ℝ] EndSpace →L[ℝ] EndSpace) instance to shorten typeclass synthesis.

Equations

• EulerPacketCofactor.instPacketCofactorOperator5 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCofactor.instPacketCofactorOperator6 : NormedSpace ℝ (EndSpace →L[ℝ] EndSpace →L[ℝ] EndSpace)

Cache the standard NormedSpace ℝ (EndSpace →L[ℝ] EndSpace →L[ℝ] EndSpace) instance to shorten typeclass synthesis.

Equations

• EulerPacketCofactor.instPacketCofactorOperator6 = inferInstance

noncomputable def EulerPacketCofactor.basis (i : Fin 3) : EulerSmoothLimit.Space

Basis, given by EuclideanSpace.single i 1.

Equations

• EulerPacketCofactor.basis i = EuclideanSpace.single i 1

@[simp]

theorem EulerPacketCofactor.basis_norm (i : Fin 3) : ‖basis i‖ = 1

noncomputable def EulerPacketCofactor.rowLinear (i : Fin 3) : EulerSmoothLimit.Space →ₗ[ℝ] EndSpace

Row linear, bundling toFun, map_add, map_smul.

Equations

• EulerPacketCofactor.rowLinear i = { toFun := fun (a : EulerSmoothLimit.Space) => ((innerSL ℝ) a).smulRight (EulerPacketCofactor.basis i), map_add' := ⋯, map_smul' := ⋯ }

theorem EulerPacketCofactor.rowLinear_norm (i : Fin 3) (a : EulerSmoothLimit.Space) : ‖(rowLinear i) a‖ ≤ ‖a‖

noncomputable def EulerPacketCofactor.rowOperator (i : Fin 3) : EulerSmoothLimit.Space →L[ℝ] EndSpace

Row operator, given by (rowLinear i).mkContinuous 1 (fun a => by simpa only [one_mul] using rowLinear_norm i a).

Equations

• EulerPacketCofactor.rowOperator i = (EulerPacketCofactor.rowLinear i).mkContinuous 1 ⋯

@[simp]

theorem EulerPacketCofactor.rowOperator_apply (i : Fin 3) (a v : EulerSmoothLimit.Space) : ((rowOperator i) a) v = inner ℝ a v • basis i

theorem EulerPacketCofactor.rowOperator_norm (i : Fin 3) (a : EulerSmoothLimit.Space) : ‖(rowOperator i) a‖ ≤ ‖a‖

noncomputable def EulerPacketCofactor.cofactorValue (A B : EndSpace) : EndSpace

Cofactor value, constructed using rowOperator.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerPacketCofactor.cofactorLinear : EndSpace →ₗ[ℝ] EndSpace →ₗ[ℝ] EndSpace

Cofactor linear, bundling toFun, map_add, map_smul, map_add and the required compatibility proofs.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerPacketCofactor.cofactorValue_norm (A B : EndSpace) : ‖cofactorValue A B‖ ≤ 3 * ‖A‖ * ‖B‖

noncomputable def EulerPacketCofactor.cofactorBilinear : EndSpace →L[ℝ] EndSpace →L[ℝ] EndSpace

Cofactor bilinear, given by cofactorLinear.mkContinuous₂ 3 cofactorValue_norm.

Equations

• EulerPacketCofactor.cofactorBilinear = EulerPacketCofactor.cofactorLinear.mkContinuous₂ 3 EulerPacketCofactor.cofactorValue_norm

@[simp]

theorem EulerPacketCofactor.cofactorBilinear_apply (A B : EndSpace) : (cofactorBilinear A) B = cofactorValue A B

theorem EulerPacketCofactor.cofactorBilinear_norm : ‖cofactorBilinear‖ ≤ 3

noncomputable def EulerPacketCofactor.adjugate (A : EndSpace) : EndSpace

Adjugate, given by cofactorBilinear A A.

Equations

• EulerPacketCofactor.adjugate A = (EulerPacketCofactor.cofactorBilinear A) A

theorem EulerPacketCofactor.adjugate_norm (A : EndSpace) : ‖adjugate A‖ ≤ 3 * ‖A‖ ^ 2

theorem EulerPacketCofactor.operatorMatrix_adjugate (A : EndSpace) : EulerPacketPiola.operatorMatrix (adjugate A) = Matrix.adjugate (EulerPacketPiola.operatorMatrix A)

theorem EulerPacketCofactor.operatorMatrix_injective : Function.Injective EulerPacketPiola.operatorMatrix

theorem EulerPacketCofactor.adjugate_comp (A : EndSpace) (hdet : Matrix.det (EulerPacketPiola.operatorMatrix A) = 1) : adjugate A ∘SL A = ContinuousLinearMap.id ℝ EulerSmoothLimit.Space

theorem EulerPacketCofactor.comp_adjugate (A : EndSpace) (hdet : Matrix.det (EulerPacketPiola.operatorMatrix A) = 1) : A ∘SL adjugate A = ContinuousLinearMap.id ℝ EulerSmoothLimit.Space

theorem EulerPacketCofactor.inverse_eq_adjugate (A I : EndSpace) (hdet : Matrix.det (EulerPacketPiola.operatorMatrix A) = 1) (hI : ∀ (v : EulerSmoothLimit.Space), I (A v) = v) : I = adjugate A