NYLL
Module

ChoiceCountSystem.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.LogExpSeries.FormalCoreBase.ChoiceCountSystem
11 declarations indexed from sourceView source ↗

Module documentation

Coordinate equations for basic-factor choices

This module derives the three coordinate and total-count equations satisfied by a choice of the basic factors in X + Y + XY.

Imports1
Imported by3

Declarations

def

formalLogOnePlusProductArgumentBasicFactorLabelCountChoices

L27 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorLabelCountChoices
Documentation

Basic-factor sequences with the three label counts forced by q and the target exponent vector e.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
def formalLogOnePlusProductArgumentBasicFactorLabelCountChoices
    (q : ℕ) (e : Fin 2 →₀ ℕ) :
    Finset (ℕ →₀ (Fin 2 →₀ ℕ))
theorem

mem_formalLogOnePlusProductArgumentBasicFactorLabelCountChoices

L46 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.mem_formalLogOnePlusProductArgumentBasicFactorLabelCountChoices
Documentation

Characterizes l ∈ formalLogOnePlusProductArgumentBasicFactorLabelCountChoices q e by the equivalent condition l ∈ formalLogOnePlusProductArgumentBasicFactorProductChoices q ∧ formalLogOnePlusProductArgumentBasicFactorLabelCount q l 0 = q - e (1 : Fin 2) ∧ formalLogOnePlusProductArgumentBasicFactorLabelCount q l 1 = q - e (0 : Fin 2) ∧ formalLogOnePlusProductArgumentBasicFactorLabelCount q l 2 = e (0 : Fin 2) + e (1 : Fin 2) - q.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem mem_formalLogOnePlusProductArgumentBasicFactorLabelCountChoices
    {q : ℕ} {e : Fin 2 →₀ ℕ} {l : ℕ →₀ (Fin 2 →₀ ℕ)} :
    l ∈ formalLogOnePlusProductArgumentBasicFactorLabelCountChoices q e ↔
      l ∈ formalLogOnePlusProductArgumentBasicFactorProductChoices q ∧
        formalLogOnePlusProductArgumentBasicFactorLabelCount q l 0 =
            q - e (1 : Fin 2) ∧
          formalLogOnePlusProductArgumentBasicFactorLabelCount q l 1 =
            q - e (0 : Fin 2) ∧
            formalLogOnePlusProductArgumentBasicFactorLabelCount q l 2 =
              e (0 : Fin 2) + e (1 : Fin 2) - q
theorem

formalLogOnePlusProductArgumentBasicFactor_left_coord

L63 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactor_left_coord
Documentation

Establishes the identity m (0 : Fin 2) = (if m = Finsupp.single (0 : Fin 2) 1 then 1 else 0) + (if m = Finsupp.single (0 : Fin 2) 1 + Finsupp.single (1 : Fin 2) 1 then 1 else 0).

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · full declaration
theorem formalLogOnePlusProductArgumentBasicFactor_left_coord
    {m : Fin 2 →₀ ℕ}
    (hm : formalLogOnePlusProductArgumentBasicFactor m) :
    m (0 : Fin 2) =
      (if m = Finsupp.single (0 : Fin 2) 1 then 1 else 0) +
        (if m =
            Finsupp.single (0 : Fin 2) 1 +
              Finsupp.single (1 : Fin 2) 1
          then 1 else 0) := by
  rcases hm with hleft | hright | hmixed
  · simp [hleft]
  · have hrightLeft :
        Finsupp.single (1 : Fin 2) 1 ≠
          Finsupp.single (0 : Fin 2) 1 :=
      finsupp_fin_two_single_left_ne_single_right.symm
    simp [hright, hrightLeft]
  · have hmixedLeft :
        Finsupp.single (0 : Fin 2) 1 +
            Finsupp.single (1 : Fin 2) 1 ≠
          Finsupp.single (0 : Fin 2) 1 :=
      finsupp_fin_two_single_left_ne_mixed.symm
    simp [hmixed, hmixedLeft]
theorem

formalLogOnePlusProductArgumentBasicFactor_right_coord

L90 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactor_right_coord
Documentation

Establishes the identity m (1 : Fin 2) = (if m = Finsupp.single (1 : Fin 2) 1 then 1 else 0) + (if m = Finsupp.single (0 : Fin 2) 1 + Finsupp.single (1 : Fin 2) 1 then 1 else 0).

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · full declaration
theorem formalLogOnePlusProductArgumentBasicFactor_right_coord
    {m : Fin 2 →₀ ℕ}
    (hm : formalLogOnePlusProductArgumentBasicFactor m) :
    m (1 : Fin 2) =
      (if m = Finsupp.single (1 : Fin 2) 1 then 1 else 0) +
        (if m =
            Finsupp.single (0 : Fin 2) 1 +
              Finsupp.single (1 : Fin 2) 1
          then 1 else 0) := by
  rcases hm with hleft | hright | hmixed
  · simp [hleft, finsupp_fin_two_single_left_ne_single_right]
  · simp [hright]
  · have hmixedRight :
        Finsupp.single (0 : Fin 2) 1 +
            Finsupp.single (1 : Fin 2) 1 ≠
          Finsupp.single (1 : Fin 2) 1 :=
      finsupp_fin_two_single_right_ne_mixed.symm
    simp [hmixed, hmixedRight]
theorem

formalLogOnePlusProductArgumentBasicFactor_total_indicator

L114 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactor_total_indicator
Documentation

Establishes the identity (if m = Finsupp.single (0 : Fin 2) 1 then 1 else 0) + (if m = Finsupp.single (1 : Fin 2) 1 then 1 else 0) + (if m = Finsupp.single (0 : Fin 2) 1 + Finsupp.single (1 : Fin 2) 1 then 1 else 0) = 1.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · full declaration
theorem formalLogOnePlusProductArgumentBasicFactor_total_indicator
    {m : Fin 2 →₀ ℕ}
    (hm : formalLogOnePlusProductArgumentBasicFactor m) :
    (if m = Finsupp.single (0 : Fin 2) 1 then 1 else 0) +
          (if m = Finsupp.single (1 : Fin 2) 1 then 1 else 0) +
        (if m =
            Finsupp.single (0 : Fin 2) 1 +
              Finsupp.single (1 : Fin 2) 1
          then 1 else 0) =
      1 := by
  rcases hm with hleft | hright | hmixed
  · simp [hleft, finsupp_fin_two_single_left_ne_single_right]
  · have hrightLeft :
        Finsupp.single (1 : Fin 2) 1 ≠
          Finsupp.single (0 : Fin 2) 1 :=
      finsupp_fin_two_single_left_ne_single_right.symm
    simp [hright, hrightLeft]
  · have hmixedLeft :
        Finsupp.single (0 : Fin 2) 1 +
            Finsupp.single (1 : Fin 2) 1 ≠
          Finsupp.single (0 : Fin 2) 1 :=
      finsupp_fin_two_single_left_ne_mixed.symm
    have hmixedRight :
        Finsupp.single (0 : Fin 2) 1 +
            Finsupp.single (1 : Fin 2) 1 ≠
          Finsupp.single (1 : Fin 2) 1 :=
      finsupp_fin_two_single_right_ne_mixed.symm
    simp [hmixed, hmixedLeft, hmixedRight]
theorem

formalLogOnePlusProductArgument_leftCoord_sum_eq_choiceCounts

L148 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_leftCoord_sum_eq_choiceCounts
Documentation

Establishes the identity (∑ i ∈ Finset.range q, l i (0 : Fin 2)) = formalLogOnePlusProductArgumentLeftChoiceCount q l + formalLogOnePlusProductArgumentMixedChoiceCount q l.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_leftCoord_sum_eq_choiceCounts
    {q : ℕ} {l : ℕ →₀ (Fin 2 →₀ ℕ)}
    (hbasic : ∀ i ∈ Finset.range q,
      formalLogOnePlusProductArgumentBasicFactor (l i)) :
    (∑ i ∈ Finset.range q, l i (0 : Fin 2)) =
      formalLogOnePlusProductArgumentLeftChoiceCount q l +
        formalLogOnePlusProductArgumentMixedChoiceCount q l
theorem

formalLogOnePlusProductArgument_rightCoord_sum_eq_choiceCounts

L166 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_rightCoord_sum_eq_choiceCounts
Documentation

Establishes the identity (∑ i ∈ Finset.range q, l i (1 : Fin 2)) = formalLogOnePlusProductArgumentRightChoiceCount q l + formalLogOnePlusProductArgumentMixedChoiceCount q l.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_rightCoord_sum_eq_choiceCounts
    {q : ℕ} {l : ℕ →₀ (Fin 2 →₀ ℕ)}
    (hbasic : ∀ i ∈ Finset.range q,
      formalLogOnePlusProductArgumentBasicFactor (l i)) :
    (∑ i ∈ Finset.range q, l i (1 : Fin 2)) =
      formalLogOnePlusProductArgumentRightChoiceCount q l +
        formalLogOnePlusProductArgumentMixedChoiceCount q l
theorem

formalLogOnePlusProductArgument_totalChoiceCount_eq

L184 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_totalChoiceCount_eq
Documentation

Establishes the identity formalLogOnePlusProductArgumentLeftChoiceCount q l + formalLogOnePlusProductArgumentRightChoiceCount q l + formalLogOnePlusProductArgumentMixedChoiceCount q l = q.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_totalChoiceCount_eq
    {q : ℕ} {l : ℕ →₀ (Fin 2 →₀ ℕ)}
    (hbasic : ∀ i ∈ Finset.range q,
      formalLogOnePlusProductArgumentBasicFactor (l i)) :
    formalLogOnePlusProductArgumentLeftChoiceCount q l +
        formalLogOnePlusProductArgumentRightChoiceCount q l +
      formalLogOnePlusProductArgumentMixedChoiceCount q l =
    q
theorem

formalLogOnePlusProductArgument_choiceCounts_left_add_mixed_eq

L215 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_choiceCounts_left_add_mixed_eq
Documentation

Establishes the identity formalLogOnePlusProductArgumentLeftChoiceCount q l + formalLogOnePlusProductArgumentMixedChoiceCount q l = e (0 : Fin 2).

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_choiceCounts_left_add_mixed_eq
    {q : ℕ} {e : Fin 2 →₀ ℕ} {l : ℕ →₀ (Fin 2 →₀ ℕ)}
    (hl : l ∈ Finset.finsuppAntidiag (Finset.range q) e)
    (hbasic : ∀ i ∈ Finset.range q,
      formalLogOnePlusProductArgumentBasicFactor (l i)) :
    formalLogOnePlusProductArgumentLeftChoiceCount q l +
      formalLogOnePlusProductArgumentMixedChoiceCount q l =
        e (0 : Fin 2)
theorem

formalLogOnePlusProductArgument_choiceCounts_right_add_mixed_eq

L232 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_choiceCounts_right_add_mixed_eq
Documentation

Establishes the identity formalLogOnePlusProductArgumentRightChoiceCount q l + formalLogOnePlusProductArgumentMixedChoiceCount q l = e (1 : Fin 2).

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_choiceCounts_right_add_mixed_eq
    {q : ℕ} {e : Fin 2 →₀ ℕ} {l : ℕ →₀ (Fin 2 →₀ ℕ)}
    (hl : l ∈ Finset.finsuppAntidiag (Finset.range q) e)
    (hbasic : ∀ i ∈ Finset.range q,
      formalLogOnePlusProductArgumentBasicFactor (l i)) :
    formalLogOnePlusProductArgumentRightChoiceCount q l +
      formalLogOnePlusProductArgumentMixedChoiceCount q l =
        e (1 : Fin 2)
theorem

formalLogOnePlusProductArgument_choiceCounts_system

L254 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_choiceCounts_system
Documentation

Establishes the identity formalLogOnePlusProductArgumentLeftChoiceCount q l + formalLogOnePlusProductArgumentMixedChoiceCount q l = e (0 : Fin 2) ∧ formalLogOnePlusProductArgumentRightChoiceCount q l + formalLogOnePlusProductArgumentMixedChoiceCount q l = e (1 : Fin 2) ∧ formalLogOnePlusProductArgumentLeftChoiceCount q l + formalLogOnePlusProductArgumentRightChoiceCount q l + formalLogOnePlusProductArgumentMixedChoiceCount q l = q.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_choiceCounts_system
    {q : ℕ} {e : Fin 2 →₀ ℕ} {l : ℕ →₀ (Fin 2 →₀ ℕ)}
    (hl : l ∈ Finset.finsuppAntidiag (Finset.range q) e)
    (hbasic : ∀ i ∈ Finset.range q,
      formalLogOnePlusProductArgumentBasicFactor (l i)) :
    formalLogOnePlusProductArgumentLeftChoiceCount q l +
          formalLogOnePlusProductArgumentMixedChoiceCount q l =
        e (0 : Fin 2) ∧
      formalLogOnePlusProductArgumentRightChoiceCount q l +
          formalLogOnePlusProductArgumentMixedChoiceCount q l =
        e (1 : Fin 2) ∧
      formalLogOnePlusProductArgumentLeftChoiceCount q l +
            formalLogOnePlusProductArgumentRightChoiceCount q l +
          formalLogOnePlusProductArgumentMixedChoiceCount q l =
        q

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.