Entrywise translated expansion of the actual minor
ProvedOAI.PiExponent.LiteralAnalytic.TranslatedExpansion.actualMinor_entry_eq_choice_sumnumber-theoryopenai-pi-exponent-017
Every selected matrix entry is the finite weighted sum of its translated row-choice contributions. Updating f at the selected row exposes the corresponding choice-matrix entry without changing the other rows.
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.actualMinor_entry_eq_choice_sum
{nu : ℝ} (d : FixedData nu) {H : ℝ} (hH : 0 < H)
(selection : Row d H → Column d H) (f : ChoiceFamily d H)
(r c : Row d H) :
actualMinor d H selection r c =
∑ t : RowChoice d H r,
choiceScalar d r t *
choiceMatrix d selection (Function.update f r t) r c := by sorrySource