NYLL
Module

ChoicePositions.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.LogExpSeries.FormalCoreBase.ChoicePositions
17 declarations indexed from sourceView source ↗

Module documentation

Realizing formal-product choices by position sets

This module constructs a basic-factor choice from its mixed and left position sets and proves the resulting position-count formulas.

Imports1
Imported by2

Declarations

def

formalLogOnePlusProductArgumentBasicFactorLeft

L26 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorLeft
Documentation

The left basic exponent vector.

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 formalLogOnePlusProductArgumentBasicFactorLeft :
    Fin 2 →₀ ℕ
def

formalLogOnePlusProductArgumentBasicFactorRight

L31 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorRight
Documentation

The right basic exponent vector.

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 formalLogOnePlusProductArgumentBasicFactorRight :
    Fin 2 →₀ ℕ
def

formalLogOnePlusProductArgumentBasicFactorMixed

L36 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorMixed
Documentation

The mixed basic exponent vector.

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 formalLogOnePlusProductArgumentBasicFactorMixed :
    Fin 2 →₀ ℕ
theorem

formalLogOnePlusProductArgumentBasicFactorLabel_eq_two_iff_of_basic

L44 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorLabel_eq_two_iff_of_basic
Documentation

Characterizes formalLogOnePlusProductArgumentBasicFactorLabel m = (2 : Fin 3) by the equivalent condition m = formalLogOnePlusProductArgumentBasicFactorMixed.

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_two_iff_of_basic
    {m : Fin 2 →₀ ℕ}
    (hm : formalLogOnePlusProductArgumentBasicFactor m) :
    formalLogOnePlusProductArgumentBasicFactorLabel m = (2 : Fin 3) ↔
      m = formalLogOnePlusProductArgumentBasicFactorMixed
def

formalLogOnePlusProductArgumentChoiceFromMixedLeft

L60 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentChoiceFromMixedLeft
Documentation

The basic-factor sequence with mixed positions M, left positions L, and right factors in every remaining position below 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
def formalLogOnePlusProductArgumentChoiceFromMixedLeft
    (q : ℕ) (M L : Finset ℕ) : ℕ →₀ (Fin 2 →₀ ℕ)
theorem

formalLogOnePlusProductArgumentChoiceFromMixedLeft_apply_of_mem

L81 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentChoiceFromMixedLeft_apply_of_mem
Documentation

Establishes the identity formalLogOnePlusProductArgumentChoiceFromMixedLeft q M L i = if i ∈ M then formalLogOnePlusProductArgumentBasicFactorMixed else if i ∈ L then formalLogOnePlusProductArgumentBasicFactorLeft else formalLogOnePlusProductArgumentBasicFactorRight.

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 formalLogOnePlusProductArgumentChoiceFromMixedLeft_apply_of_mem
    {q : ℕ} {M L : Finset ℕ} {i : ℕ} (hi : i ∈ Finset.range q) :
    formalLogOnePlusProductArgumentChoiceFromMixedLeft q M L i =
      if i ∈ M then formalLogOnePlusProductArgumentBasicFactorMixed
      else if i ∈ L then formalLogOnePlusProductArgumentBasicFactorLeft
      else formalLogOnePlusProductArgumentBasicFactorRight := by
  have hlt : i < q := Finset.mem_range.mp hi
  simp [formalLogOnePlusProductArgumentChoiceFromMixedLeft, hlt]
theorem

formalLogOnePlusProductArgumentChoiceFromMixedLeft_apply_of_not_mem

L91 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentChoiceFromMixedLeft_apply_of_not_mem
Documentation

Establishes the identity formalLogOnePlusProductArgumentChoiceFromMixedLeft q M L i = 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 formalLogOnePlusProductArgumentChoiceFromMixedLeft_apply_of_not_mem
    {q : ℕ} {M L : Finset ℕ} {i : ℕ} (hi : i ∉ Finset.range q) :
    formalLogOnePlusProductArgumentChoiceFromMixedLeft q M L i = 0
def

formalLogOnePlusProductArgumentMixedPositions

L98 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentMixedPositions
Documentation

Positions below q at which l has the mixed-factor label.

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

formalLogOnePlusProductArgumentLeftPositions

L104 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentLeftPositions
Documentation

Positions below q at which l has the left-factor label.

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

formalLogOnePlusProductArgumentRightPositions

L110 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentRightPositions
Documentation

Positions below q at which l has the right-factor label.

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

formalLogOnePlusProductArgumentMixedPositions_card

L119 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentMixedPositions_card
Documentation

Establishes the identity (formalLogOnePlusProductArgumentMixedPositions q l).card = 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 formalLogOnePlusProductArgumentMixedPositions_card
    (q : ℕ) (l : ℕ →₀ (Fin 2 →₀ ℕ)) :
    (formalLogOnePlusProductArgumentMixedPositions q l).card =
      formalLogOnePlusProductArgumentBasicFactorLabelCount q l 2
theorem

formalLogOnePlusProductArgumentLeftPositions_card

L130 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentLeftPositions_card
Documentation

Establishes the identity (formalLogOnePlusProductArgumentLeftPositions q l).card = 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 formalLogOnePlusProductArgumentLeftPositions_card
    (q : ℕ) (l : ℕ →₀ (Fin 2 →₀ ℕ)) :
    (formalLogOnePlusProductArgumentLeftPositions q l).card =
      formalLogOnePlusProductArgumentBasicFactorLabelCount q l 0
theorem

formalLogOnePlusProductArgumentRightPositions_card

L141 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentRightPositions_card
Documentation

Establishes the identity (formalLogOnePlusProductArgumentRightPositions q l).card = 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 formalLogOnePlusProductArgumentRightPositions_card
    (q : ℕ) (l : ℕ →₀ (Fin 2 →₀ ℕ)) :
    (formalLogOnePlusProductArgumentRightPositions q l).card =
      formalLogOnePlusProductArgumentBasicFactorLabelCount q l 1
theorem

formalLogOnePlusProductArgumentMixedPositions_choiceFromMixedLeft

L152 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentMixedPositions_choiceFromMixedLeft
Documentation

Establishes the identity formalLogOnePlusProductArgumentMixedPositions q (formalLogOnePlusProductArgumentChoiceFromMixedLeft q M L) = 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 formalLogOnePlusProductArgumentMixedPositions_choiceFromMixedLeft
    {q : ℕ} {M L : Finset ℕ} (hM : M ⊆ Finset.range q) :
    formalLogOnePlusProductArgumentMixedPositions q
        (formalLogOnePlusProductArgumentChoiceFromMixedLeft q M L) = M
theorem

formalLogOnePlusProductArgumentLeftPositions_choiceFromMixedLeft

L181 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentLeftPositions_choiceFromMixedLeft
Documentation

Establishes the identity formalLogOnePlusProductArgumentLeftPositions q (formalLogOnePlusProductArgumentChoiceFromMixedLeft q M L) = 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 formalLogOnePlusProductArgumentLeftPositions_choiceFromMixedLeft
    {q : ℕ} {M L : Finset ℕ} (hL : L ⊆ Finset.range q \ M) :
    formalLogOnePlusProductArgumentLeftPositions q
        (formalLogOnePlusProductArgumentChoiceFromMixedLeft q M L) = L
theorem

formalLogOnePlusProductArgumentRightPositions_choiceFromMixedLeft

L211 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentRightPositions_choiceFromMixedLeft
Documentation

Establishes the identity formalLogOnePlusProductArgumentRightPositions q (formalLogOnePlusProductArgumentChoiceFromMixedLeft q M L) = Finset.range q \ (M ∪ 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 formalLogOnePlusProductArgumentRightPositions_choiceFromMixedLeft
    {q : ℕ} {M L : Finset ℕ} (hL : L ⊆ Finset.range q \ M) :
    formalLogOnePlusProductArgumentRightPositions q
        (formalLogOnePlusProductArgumentChoiceFromMixedLeft q M L) =
      Finset.range q \ (M ∪ L)
theorem

formalLogOnePlusProductArgumentRightPositions_choiceFromMixedLeft_card

L251 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentRightPositions_choiceFromMixedLeft_card
Documentation

Establishes the identity (formalLogOnePlusProductArgumentRightPositions q (formalLogOnePlusProductArgumentChoiceFromMixedLeft q M L)).card = q - a.

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 formalLogOnePlusProductArgumentRightPositions_choiceFromMixedLeft_card
    {q a b : ℕ} {M L : Finset ℕ}
    (hMsub : M ⊆ Finset.range q) (hMcard : M.card = a + b - q)
    (hLsub : L ⊆ Finset.range q \ M) (hLcard : L.card = q - b)
    (hleft : a ≤ q) (hright : b ≤ q) (hsum : q ≤ a + b) :
    (formalLogOnePlusProductArgumentRightPositions q
      (formalLogOnePlusProductArgumentChoiceFromMixedLeft q M L)).card =
        q - a

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