Module

ExplicitChoiceCounts.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.LogExpSeries.FormalCoreBase.ExplicitChoiceCounts

10 declarations indexed from sourceView source ↗

Module documentation

Explicit counts for basic-factor choices

This module solves the coordinate-count system and relates its solution to the label-count and multinomial choice spaces.

Imports1

Nyll.ValuedFieldTheory.LocalField.Analytic.LogExpSeries.FormalCoreBase.ChoiceCountSystem

Imported by3

theorem

formalLogOnePlusProductArgument_choiceCounts_total_add_mixed_eq_coord_sum

L29 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_choiceCounts_total_add_mixed_eq_coord_sum

Documentation

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

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_total_add_mixed_eq_coord_sum
    {q : ℕ} {e : Fin 2 →₀ ℕ} {l : ℕ →₀ (Fin 2 →₀ ℕ)}
    (hl : l ∈ Finset.finsuppAntidiag (Finset.range q) e)
    (hbasic : ∀ i ∈ Finset.range q,
      formalLogOnePlusProductArgumentBasicFactor (l i)) :
    q + formalLogOnePlusProductArgumentMixedChoiceCount q l =
      e (0 : Fin 2) + e (1 : Fin 2)

theorem

formalLogOnePlusProductArgument_choiceCounts_q_le_coord_sum

L57 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_choiceCounts_q_le_coord_sum

Documentation

Proves the bound q ≤ e (0 : Fin 2) + 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_q_le_coord_sum
    {q : ℕ} {e : Fin 2 →₀ ℕ} {l : ℕ →₀ (Fin 2 →₀ ℕ)}
    (hl : l ∈ Finset.finsuppAntidiag (Finset.range q) e)
    (hbasic : ∀ i ∈ Finset.range q,
      formalLogOnePlusProductArgumentBasicFactor (l i)) :
    q ≤ e (0 : Fin 2) + e (1 : Fin 2)

theorem

formalLogOnePlusProductArgument_mixedChoiceCount_eq_coord_sum_sub_q

L72 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_mixedChoiceCount_eq_coord_sum_sub_q

Documentation

Establishes the identity formalLogOnePlusProductArgumentMixedChoiceCount q l = 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 formalLogOnePlusProductArgument_mixedChoiceCount_eq_coord_sum_sub_q
    {q : ℕ} {e : Fin 2 →₀ ℕ} {l : ℕ →₀ (Fin 2 →₀ ℕ)}
    (hl : l ∈ Finset.finsuppAntidiag (Finset.range q) e)
    (hbasic : ∀ i ∈ Finset.range q,
      formalLogOnePlusProductArgumentBasicFactor (l i)) :
    formalLogOnePlusProductArgumentMixedChoiceCount q l =
      e (0 : Fin 2) + e (1 : Fin 2) - q

theorem

formalLogOnePlusProductArgument_leftChoiceCount_eq_q_sub_right_coord

L92 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_leftChoiceCount_eq_q_sub_right_coord

Documentation

Establishes the identity formalLogOnePlusProductArgumentLeftChoiceCount q l = q - 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_leftChoiceCount_eq_q_sub_right_coord
    {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 =
      q - e (1 : Fin 2)

theorem

formalLogOnePlusProductArgument_rightChoiceCount_eq_q_sub_left_coord

L131 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_rightChoiceCount_eq_q_sub_left_coord

Documentation

Establishes the identity formalLogOnePlusProductArgumentRightChoiceCount q l = q - 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_rightChoiceCount_eq_q_sub_left_coord
    {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 =
      q - e (0 : Fin 2)

theorem

formalLogOnePlusProductArgument_choiceCounts_explicit

L171 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_choiceCounts_explicit

Documentation

Establishes the identity formalLogOnePlusProductArgumentLeftChoiceCount q l = q - e (1 : Fin 2) ∧ formalLogOnePlusProductArgumentRightChoiceCount q l = q - e (0 : Fin 2) ∧ formalLogOnePlusProductArgumentMixedChoiceCount q l = 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 formalLogOnePlusProductArgument_choiceCounts_explicit
    {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 =
          q - e (1 : Fin 2) ∧
      formalLogOnePlusProductArgumentRightChoiceCount q l =
          q - e (0 : Fin 2) ∧
        formalLogOnePlusProductArgumentMixedChoiceCount q l =
          e (0 : Fin 2) + e (1 : Fin 2) - q

theorem

formalLogOnePlusProductArgument_labelCounts_explicit

L195 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_labelCounts_explicit

Documentation

Establishes the identity 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 formalLogOnePlusProductArgument_labelCounts_explicit
    {q : ℕ} {e : Fin 2 →₀ ℕ} {l : ℕ →₀ (Fin 2 →₀ ℕ)}
    (hl : l ∈ Finset.finsuppAntidiag (Finset.range q) e)
    (hbasic : ∀ i ∈ Finset.range q,
      formalLogOnePlusProductArgumentBasicFactor (l i)) :
    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

formalLogOnePlusProductArgumentBasicFactorChoices_labelCounts_explicit

L226 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorChoices_labelCounts_explicit

Documentation

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 formalLogOnePlusProductArgumentBasicFactorChoices_labelCounts_explicit
    {q : ℕ} {e : Fin 2 →₀ ℕ} {l : ℕ →₀ (Fin 2 →₀ ℕ)}
    (hl : l ∈ formalLogOnePlusProductArgumentBasicFactorChoices q e) :
    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

formalLogOnePlusProductArgumentBasicFactorChoices_subset_labelCountChoices

L239 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorChoices_subset_labelCountChoices

Documentation

Every basic-factor choice satisfies the corresponding three label-count constraints.

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 formalLogOnePlusProductArgumentBasicFactorChoices_subset_labelCountChoices
    (q : ℕ) (e : Fin 2 →₀ ℕ) :
    formalLogOnePlusProductArgumentBasicFactorChoices q e ⊆
      formalLogOnePlusProductArgumentBasicFactorLabelCountChoices q e

theorem

formalLogOnePlusProductArgumentBasicFactorChoices_card_le_labelCountChoices

L258 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorChoices_card_le_labelCountChoices

Documentation

Proves the bound (formalLogOnePlusProductArgumentBasicFactorChoices q e).card ≤ (formalLogOnePlusProductArgumentBasicFactorLabelCountChoices q e).card.

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 formalLogOnePlusProductArgumentBasicFactorChoices_card_le_labelCountChoices
    (q : ℕ) (e : Fin 2 →₀ ℕ) :
    (formalLogOnePlusProductArgumentBasicFactorChoices q e).card ≤
      (formalLogOnePlusProductArgumentBasicFactorLabelCountChoices q e).card

Module documentation

Explicit counts for basic-factor choices

Declarations