Canonical translated determinant expansion of the actual minor
ProvedOAI.PiExponent.LiteralAnalytic.TranslatedExpansion.minor_eq_sumnumber-theoryopenai-pi-exponent-017
For positive H, the actual minor determinant equals the sum of the canonical translated scalar-product times period-matrix determinant over all rowwise choice families.
Preamble
import Definitions.Def_OAI_NumberTheory_PiExponent_Analysis_TranslatedExpansionTerms open scoped BigOperators Topology open Filter open OAI.PiExponent OAI.PiExponent.DeterminantContradiction open OAI.PiExponent.LiteralAnalytic open OAI.PiExponent.LiteralAnalytic.TranslatedExpansion
Formal statement
theorem OAI.PiExponent.LiteralAnalytic.TranslatedExpansion.minor_eq_sum
{nu : ℝ} (d : FixedData nu) {H : ℝ} (hH : 0 < H)
(selection : Row d H → Column d H) :
(actualMinor d H selection).det = ∑ f : ChoiceFamily d H, summand d selection f := by sorrySource