Module

BasicFactors.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.LogExpSeries.FormalCoreBase.BasicFactors

23 declarations indexed from sourceView source ↗

Module documentation

Basic factors in the formal logarithm product argument

This module packages the three possible nonzero monomial factors and their finite choice spaces.

Imports1

Nyll.ValuedFieldTheory.LocalField.Analytic.LogExpSeries.FormalCoreBase.ProductArgument

Imported by3

def

formalLogOnePlusProductArgumentBasicFactor

L26 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactor

Documentation

The three exponent vectors with nonzero coefficient in X + Y + XY.

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 formalLogOnePlusProductArgumentBasicFactor
    (m : Fin 2 →₀ ℕ) : Prop

def

formalLogOnePlusProductArgumentBasicFactorFinset

L35 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorFinset

Documentation

The finite set of the left, right, and mixed basic exponent vectors.

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 formalLogOnePlusProductArgumentBasicFactorFinset :
    Finset (Fin 2 →₀ ℕ)

theorem

mem_formalLogOnePlusProductArgumentBasicFactorFinset

L48 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.mem_formalLogOnePlusProductArgumentBasicFactorFinset

Documentation

Characterizes m ∈ formalLogOnePlusProductArgumentBasicFactorFinset by the equivalent condition formalLogOnePlusProductArgumentBasicFactor m.

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_formalLogOnePlusProductArgumentBasicFactorFinset
    {m : Fin 2 →₀ ℕ} :
    m ∈ formalLogOnePlusProductArgumentBasicFactorFinset ↔
      formalLogOnePlusProductArgumentBasicFactor m

theorem

formalLogOnePlusProductArgumentBasicFactorFinset_card

L57 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorFinset_card

Documentation

Establishes the identity formalLogOnePlusProductArgumentBasicFactorFinset.card = 3.

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 formalLogOnePlusProductArgumentBasicFactorFinset_card :
    formalLogOnePlusProductArgumentBasicFactorFinset.card = 3

def

formalLogOnePlusProductArgumentBasicFactorLabel

L66 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorLabel

Documentation

Labels the left, right, and mixed basic factors by 0, 1, and 2. Non-basic inputs receive the mixed label; all uses that recover a factor from its label therefore carry a basic-factor hypothesis.

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 formalLogOnePlusProductArgumentBasicFactorLabel
    (m : Fin 2 →₀ ℕ) : Fin 3

theorem

formalLogOnePlusProductArgumentBasicFactorLabel_left

L76 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorLabel_left

Documentation

Establishes the identity formalLogOnePlusProductArgumentBasicFactorLabel (Finsupp.single (0 : Fin 2) 1) = 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 · statement

theorem formalLogOnePlusProductArgumentBasicFactorLabel_left :
    formalLogOnePlusProductArgumentBasicFactorLabel
        (Finsupp.single (0 : Fin 2) 1) = 0

theorem

formalLogOnePlusProductArgumentBasicFactorLabel_right

L85 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorLabel_right

Documentation

Establishes the identity formalLogOnePlusProductArgumentBasicFactorLabel (Finsupp.single (1 : Fin 2) 1) = 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 · statement

theorem formalLogOnePlusProductArgumentBasicFactorLabel_right :
    formalLogOnePlusProductArgumentBasicFactorLabel
        (Finsupp.single (1 : Fin 2) 1) = 1

theorem

formalLogOnePlusProductArgumentBasicFactorLabel_mixed

L95 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorLabel_mixed

Documentation

Establishes the identity formalLogOnePlusProductArgumentBasicFactorLabel (Finsupp.single (0 : Fin 2) 1 + Finsupp.single (1 : Fin 2) 1) = 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 formalLogOnePlusProductArgumentBasicFactorLabel_mixed :
    formalLogOnePlusProductArgumentBasicFactorLabel
        (Finsupp.single (0 : Fin 2) 1 +
          Finsupp.single (1 : Fin 2) 1) = 2

theorem

formalLogOnePlusProductArgumentBasicFactorLabel_eq_zero

L107 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorLabel_eq_zero

Documentation

Characterizes formalLogOnePlusProductArgumentBasicFactorLabel m = (0 : Fin 3) by the equivalent condition m = Finsupp.single (0 : Fin 2) 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 · statement

theorem formalLogOnePlusProductArgumentBasicFactorLabel_eq_zero
    {m : Fin 2 →₀ ℕ} :
    formalLogOnePlusProductArgumentBasicFactorLabel m = (0 : Fin 3) ↔
      m = Finsupp.single (0 : Fin 2) 1

theorem

formalLogOnePlusProductArgumentBasicFactorLabel_eq_one

L122 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorLabel_eq_one

Documentation

Characterizes formalLogOnePlusProductArgumentBasicFactorLabel m = (1 : Fin 3) by the equivalent condition m = Finsupp.single (1 : Fin 2) 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 · statement

theorem formalLogOnePlusProductArgumentBasicFactorLabel_eq_one
    {m : Fin 2 →₀ ℕ} :
    formalLogOnePlusProductArgumentBasicFactorLabel m = (1 : Fin 3) ↔
      m = Finsupp.single (1 : Fin 2) 1

def

formalLogOnePlusProductArgumentBasicFactorProductChoices

L138 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorProductChoices

Documentation

Finitely supported sequences of q basic factors.

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 formalLogOnePlusProductArgumentBasicFactorProductChoices
    (q : ℕ) : Finset (ℕ →₀ (Fin 2 →₀ ℕ))

theorem

mem_formalLogOnePlusProductArgumentBasicFactorProductChoices

L150 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.mem_formalLogOnePlusProductArgumentBasicFactorProductChoices

Documentation

Characterizes l ∈ formalLogOnePlusProductArgumentBasicFactorProductChoices q by the equivalent condition l.support ⊆ Finset.range q ∧ ∀ i ∈ Finset.range q, formalLogOnePlusProductArgumentBasicFactor (l i).

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_formalLogOnePlusProductArgumentBasicFactorProductChoices
    {q : ℕ} {l : ℕ →₀ (Fin 2 →₀ ℕ)} :
    l ∈ formalLogOnePlusProductArgumentBasicFactorProductChoices q ↔
      l.support ⊆ Finset.range q ∧
        ∀ i ∈ Finset.range q,
          formalLogOnePlusProductArgumentBasicFactor (l i)

theorem

formalLogOnePlusProductArgumentBasicFactorProductChoices_card

L175 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorProductChoices_card

Documentation

Establishes the identity (formalLogOnePlusProductArgumentBasicFactorProductChoices q).card = 3 ^ 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 formalLogOnePlusProductArgumentBasicFactorProductChoices_card
    (q : ℕ) :
    (formalLogOnePlusProductArgumentBasicFactorProductChoices q).card =
      3 ^ q

def

formalLogOnePlusProductArgumentBasicFactorChoices

L185 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorChoices

Documentation

Sequences of q basic factors whose exponent-vector sum is 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 formalLogOnePlusProductArgumentBasicFactorChoices
    (q : ℕ) (e : Fin 2 →₀ ℕ) :
    Finset (ℕ →₀ (Fin 2 →₀ ℕ))

theorem

mem_formalLogOnePlusProductArgumentBasicFactorChoices

L200 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.mem_formalLogOnePlusProductArgumentBasicFactorChoices

Documentation

Characterizes l ∈ formalLogOnePlusProductArgumentBasicFactorChoices q e by the equivalent condition l ∈ Finset.finsuppAntidiag (Finset.range q) e ∧ ∀ i ∈ Finset.range q, formalLogOnePlusProductArgumentBasicFactor (l i).

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_formalLogOnePlusProductArgumentBasicFactorChoices
    {q : ℕ} {e : Fin 2 →₀ ℕ} {l : ℕ →₀ (Fin 2 →₀ ℕ)} :
    l ∈ formalLogOnePlusProductArgumentBasicFactorChoices q e ↔
      l ∈ Finset.finsuppAntidiag (Finset.range q) e ∧
        ∀ i ∈ Finset.range q,
          formalLogOnePlusProductArgumentBasicFactor (l i)

theorem

formalLogOnePlusProductArgumentBasicFactorChoices_card_le_three_pow

L210 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorChoices_card_le_three_pow

Documentation

Proves the bound (formalLogOnePlusProductArgumentBasicFactorChoices q e).card ≤ 3 ^ 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 formalLogOnePlusProductArgumentBasicFactorChoices_card_le_three_pow
    (q : ℕ) (e : Fin 2 →₀ ℕ) :
    (formalLogOnePlusProductArgumentBasicFactorChoices q e).card ≤ 3 ^ q

def

formalLogOnePlusProductArgumentLeftChoiceCount

L226 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentLeftChoiceCount

Documentation

The number of left factors among the first q entries of 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

def formalLogOnePlusProductArgumentLeftChoiceCount
    (q : ℕ) (l : ℕ →₀ (Fin 2 →₀ ℕ)) : ℕ

def

formalLogOnePlusProductArgumentRightChoiceCount

L232 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentRightChoiceCount

Documentation

The number of right factors among the first q entries of 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

def formalLogOnePlusProductArgumentRightChoiceCount
    (q : ℕ) (l : ℕ →₀ (Fin 2 →₀ ℕ)) : ℕ

def

formalLogOnePlusProductArgumentMixedChoiceCount

L238 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentMixedChoiceCount

Documentation

The number of mixed factors among the first q entries of 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

def formalLogOnePlusProductArgumentMixedChoiceCount
    (q : ℕ) (l : ℕ →₀ (Fin 2 →₀ ℕ)) : ℕ

def

formalLogOnePlusProductArgumentBasicFactorLabelCount

L247 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorLabelCount

Documentation

The number of entries among the first q positions with label j.

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 formalLogOnePlusProductArgumentBasicFactorLabelCount
    (q : ℕ) (l : ℕ →₀ (Fin 2 →₀ ℕ)) (j : Fin 3) : ℕ

theorem

formalLogOnePlusProductArgument_leftChoiceCount_eq_labelCount_zero

L257 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_leftChoiceCount_eq_labelCount_zero

Documentation

Establishes the identity formalLogOnePlusProductArgumentLeftChoiceCount q l = formalLogOnePlusProductArgumentBasicFactorLabelCount q l 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 · statement

theorem formalLogOnePlusProductArgument_leftChoiceCount_eq_labelCount_zero
    (q : ℕ) (l : ℕ →₀ (Fin 2 →₀ ℕ)) :
    formalLogOnePlusProductArgumentLeftChoiceCount q l =
      formalLogOnePlusProductArgumentBasicFactorLabelCount q l 0

theorem

formalLogOnePlusProductArgument_rightChoiceCount_eq_labelCount_one

L280 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_rightChoiceCount_eq_labelCount_one

Documentation

Establishes the identity formalLogOnePlusProductArgumentRightChoiceCount q l = formalLogOnePlusProductArgumentBasicFactorLabelCount q l 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 · statement

theorem formalLogOnePlusProductArgument_rightChoiceCount_eq_labelCount_one
    (q : ℕ) (l : ℕ →₀ (Fin 2 →₀ ℕ)) :
    formalLogOnePlusProductArgumentRightChoiceCount q l =
      formalLogOnePlusProductArgumentBasicFactorLabelCount q l 1

theorem

formalLogOnePlusProductArgument_mixedChoiceCount_eq_labelCount_two

L303 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_mixedChoiceCount_eq_labelCount_two

Documentation

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

Module documentation

Basic factors in the formal logarithm product argument

Declarations