Documentation

LeanPool.CarlsonFunctions.Carlson.TwoVariable.Basic

Two-variable Carlson functions #

source
def DirichletTransform.TwoVariable.pair (x y : ℂ) :
Fin 2 → ℂ

A pair, represented as a function on the canonical two-element index type.

Equations
Instances For
    source
    @[simp]
    theorem DirichletTransform.TwoVariable.pair_zero (x y : ℂ) :
    pair x y 0 = x

    The zeroth entry of a pair is its first argument.

    source
    @[simp]
    theorem DirichletTransform.TwoVariable.pair_one (x y : ℂ) :
    pair x y 1 = y

    The first entry of a pair is its second argument.

    source
    theorem DirichletTransform.TwoVariable.sum_pair (x y : ℂ) :
    ∑ i : Fin 2, pair x y i = x + y

    The sum of the entries of a pair.

    source
    def DirichletTransform.TwoVariable.swap :
    Equiv.Perm (Fin 2)

    The transposition of the two coordinates of Fin 2.

    Equations
    Instances For
      source
      @[simp]
      theorem DirichletTransform.TwoVariable.pair_comp_swap (x y : ℂ) :
      pair x y ∘ ⇑swap = pair y x

      Composing a pair with the two-coordinate transposition exchanges its entries.