NYLL
Module

FormalCore.lean

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

Module documentation

Choice-count combinatorics for the formal logarithm product

This module completes the formal logarithm core by identifying the basic-factor choices with pairs of finite position sets and evaluating their cardinality. The formal-series identities and the underlying position calculus live in FormalCoreBase.

Imports6
Imported by2

Declarations

def

formalLogOnePlusProductArgumentMixedLeftChoices

L42 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentMixedLeftChoices
Documentation

Defines formalLogOnePlusProductArgumentMixedLeftChoices.

Source context 10 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
def formalLogOnePlusProductArgumentMixedLeftChoices
    (q a b : ℕ) : Finset (Σ _ : Finset ℕ, Finset ℕ)
theorem

formalLogOnePlusProductArgumentMixedLeftChoices_card

L51 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentMixedLeftChoices_card
Documentation

Establishes the identity (formalLogOnePlusProductArgumentMixedLeftChoices q a b).card = Nat.choose q (a + b - q) * Nat.choose (q - (a + b - q)) (q - b).

Source context 10 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgumentMixedLeftChoices_card
    (q a b : ℕ) :
    (formalLogOnePlusProductArgumentMixedLeftChoices q a b).card =
      Nat.choose q (a + b - q) *
        Nat.choose (q - (a + b - q)) (q - b)
theorem

formalLogOnePlusProductArgument_toMixedLeft_mem

L81 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_toMixedLeft_mem
Documentation

Establishes the membership statement (⟨formalLogOnePlusProductArgumentMixedPositions q l, formalLogOnePlusProductArgumentLeftPositions q l⟩ : Σ _ : Finset ℕ, Finset ℕ) ∈ formalLogOnePlusProductArgumentMixedLeftChoices q (e (0 : Fin 2)) (e (1 : Fin 2)).

Source context 10 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_toMixedLeft_mem
    {q : ℕ} {e : Fin 2 →₀ ℕ} {l : ℕ →₀ (Fin 2 →₀ ℕ)}
    (hl :
      l ∈ formalLogOnePlusProductArgumentBasicFactorLabelCountChoices q e) :
    (⟨formalLogOnePlusProductArgumentMixedPositions q l,
        formalLogOnePlusProductArgumentLeftPositions q l⟩ :
      Σ _ : Finset ℕ, Finset ℕ) ∈
      formalLogOnePlusProductArgumentMixedLeftChoices q
        (e (0 : Fin 2)) (e (1 : Fin 2))
theorem

formalLogOnePlusProductArgument_fromMixedLeft_mem

L121 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_fromMixedLeft_mem
Documentation

Establishes the membership statement formalLogOnePlusProductArgumentChoiceFromMixedLeft q P.1 P.2 ∈ formalLogOnePlusProductArgumentBasicFactorLabelCountChoices q e.

Source context 10 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_fromMixedLeft_mem
    {q : ℕ} {e : Fin 2 →₀ ℕ}
    {P : Σ _ : Finset ℕ, Finset ℕ}
    (hleft : e (0 : Fin 2) ≤ q) (hright : e (1 : Fin 2) ≤ q)
    (hsum : q ≤ e (0 : Fin 2) + e (1 : Fin 2))
    (hP :
      P ∈ formalLogOnePlusProductArgumentMixedLeftChoices q
        (e (0 : Fin 2)) (e (1 : Fin 2))) :
    formalLogOnePlusProductArgumentChoiceFromMixedLeft q P.1 P.2 ∈
      formalLogOnePlusProductArgumentBasicFactorLabelCountChoices q e
theorem

formalLogOnePlusProductArgument_from_to_choice

L169 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_from_to_choice
Documentation

Establishes the identity formalLogOnePlusProductArgumentChoiceFromMixedLeft q (formalLogOnePlusProductArgumentMixedPositions q l) (formalLogOnePlusProductArgumentLeftPositions q l) = l.

Source context 10 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_from_to_choice
    {q : ℕ} {e : Fin 2 →₀ ℕ} {l : ℕ →₀ (Fin 2 →₀ ℕ)}
    (hl :
      l ∈ formalLogOnePlusProductArgumentBasicFactorLabelCountChoices q e) :
    formalLogOnePlusProductArgumentChoiceFromMixedLeft q
      (formalLogOnePlusProductArgumentMixedPositions q l)
      (formalLogOnePlusProductArgumentLeftPositions q l) = l
theorem

formalLogOnePlusProductArgument_to_from_pair

L233 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_to_from_pair
Documentation

Establishes the identity (⟨formalLogOnePlusProductArgumentMixedPositions q (formalLogOnePlusProductArgumentChoiceFromMixedLeft q P.1 P.2), formalLogOnePlusProductArgumentLeftPositions q (formalLogOnePlusProductArgumentChoiceFromMixedLeft q P.1 P.2)⟩ : Σ _ : Finset ℕ, Finset ℕ) = P.

Source context 10 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_to_from_pair
    {q : ℕ} {e : Fin 2 →₀ ℕ}
    {P : Σ _ : Finset ℕ, Finset ℕ}
    (hP :
      P ∈ formalLogOnePlusProductArgumentMixedLeftChoices q
        (e (0 : Fin 2)) (e (1 : Fin 2))) :
    (⟨formalLogOnePlusProductArgumentMixedPositions q
        (formalLogOnePlusProductArgumentChoiceFromMixedLeft q P.1 P.2),
      formalLogOnePlusProductArgumentLeftPositions q
        (formalLogOnePlusProductArgumentChoiceFromMixedLeft q P.1 P.2)⟩ :
      Σ _ : Finset ℕ, Finset ℕ) = P
theorem

formalLogOnePlusProductArgumentBasicFactorLabelCountChoices_card_eq_mixedLeftChoices_card

L257 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorLabelCountChoices_card_eq_mixedLeftChoices_card
Documentation

Establishes the identity (formalLogOnePlusProductArgumentBasicFactorLabelCountChoices q e).card = (formalLogOnePlusProductArgumentMixedLeftChoices q (e (0 : Fin 2)) (e (1 : Fin 2))).card.

Source context 10 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgumentBasicFactorLabelCountChoices_card_eq_mixedLeftChoices_card
    {q : ℕ} {e : Fin 2 →₀ ℕ}
    (hleft : e (0 : Fin 2) ≤ q) (hright : e (1 : Fin 2) ≤ q)
    (hsum : q ≤ e (0 : Fin 2) + e (1 : Fin 2)) :
    (formalLogOnePlusProductArgumentBasicFactorLabelCountChoices q e).card =
      (formalLogOnePlusProductArgumentMixedLeftChoices q
        (e (0 : Fin 2)) (e (1 : Fin 2))).card
theorem

formalLogOnePlusProductArgumentBasicFactorLabelCountChoices_subset_choices

L282 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorLabelCountChoices_subset_choices
Documentation

Under the coordinate bounds, every label-count choice is a valid basic-factor choice.

Source context 10 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgumentBasicFactorLabelCountChoices_subset_choices
    {q : ℕ} {e : Fin 2 →₀ ℕ}
    (hleft : e (0 : Fin 2) ≤ q) (hright : e (1 : Fin 2) ≤ q)
    (hsum : q ≤ e (0 : Fin 2) + e (1 : Fin 2)) :
    formalLogOnePlusProductArgumentBasicFactorLabelCountChoices q e ⊆
      formalLogOnePlusProductArgumentBasicFactorChoices q e
theorem

formalLogOnePlusProductArgumentBasicFactorChoices_card_eq_choose_mul_choose

L347 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentBasicFactorChoices_card_eq_choose_mul_choose
Documentation

Establishes the identity `(formalLogOnePlusProductArgumentBasicFactorChoices q e).card = Nat.choose q (e (0 : Fin 2) + e (1 : Fin 2) - q) * Nat.choose (q - (e (0 : Fin 2) + e (1 : Fin 2)

  • q)) (q - e (1 : Fin 2))`.
Source context 10 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgumentBasicFactorChoices_card_eq_choose_mul_choose
    {q : ℕ} {e : Fin 2 →₀ ℕ}
    (hleft : e (0 : Fin 2) ≤ q) (hright : e (1 : Fin 2) ≤ q)
    (hsum : q ≤ e (0 : Fin 2) + e (1 : Fin 2)) :
    (formalLogOnePlusProductArgumentBasicFactorChoices q e).card =
      Nat.choose q (e (0 : Fin 2) + e (1 : Fin 2) - q) *
        Nat.choose
          (q - (e (0 : Fin 2) + e (1 : Fin 2) - q))
          (q - e (1 : Fin 2))
theorem

formalLogOnePlusProductArgument_choiceCounts_left_coord_le_q

L372 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_choiceCounts_left_coord_le_q
Documentation

Proves the bound e (0 : Fin 2) ≤ q.

Source context 10 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_choiceCounts_left_coord_le_q
    {q : ℕ} {e : Fin 2 →₀ ℕ} {l : ℕ →₀ (Fin 2 →₀ ℕ)}
    (hl : l ∈ Finset.finsuppAntidiag (Finset.range q) e)
    (hbasic : ∀ i ∈ Finset.range q,
      formalLogOnePlusProductArgumentBasicFactor (l i)) :
    e (0 : Fin 2) ≤ q
theorem

formalLogOnePlusProductArgument_choiceCounts_right_coord_le_q

L401 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_choiceCounts_right_coord_le_q
Documentation

Proves the bound e (1 : Fin 2) ≤ q.

Source context 10 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_choiceCounts_right_coord_le_q
    {q : ℕ} {e : Fin 2 →₀ ℕ} {l : ℕ →₀ (Fin 2 →₀ ℕ)}
    (hl : l ∈ Finset.finsuppAntidiag (Finset.range q) e)
    (hbasic : ∀ i ∈ Finset.range q,
      formalLogOnePlusProductArgumentBasicFactor (l i)) :
    e (1 : Fin 2) ≤ q

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