self-conjugate partitions

Stream: new members

[ShaoYu]

In Mathlib, the distinct odd partitions are already defined. I'd like to know how to define self-conjugate partitions and prove that their counts are equal, but I'm not sure how to proceed.

[Kenny Lau]

(ref: https://mathworld.wolfram.com/Self-ConjugatePartition.html)

[Kenny Lau]

ShaoYu said:

In Mathlib, the distinct odd partitions are already defined. I'd like to know how to define self-conjugate partitions and prove that their counts are equal, but I'm not sure how to proceed.

I assume you would start with a definition of conjugate

[ShaoYu]

Kenny Lau said:

(ref: https://mathworld.wolfram.com/Self-ConjugatePartition.html)

I encountered some errors while trying to define it and couldn't resolve them.

import Mathlib

open Finset Nat Std List

open Multiset
open BigOperators Partition Nat List
open Function YoungDiagram



def self_conjugate' (n : ℕ) :=
  fun (μ : YoungDiagram) => if μ.cells.card = n ∧ μ.transpose.cells= μ.cells then
    {μ.cells}
  else
    Finset.empty

#check self_conjugate'


def self_conjugate (n : ℕ)  :=
  Finset.univ.filter (fun c => self_conjugate' n c).getD ∅

[Kenny Lau]

@ShaoYu I'm not sure what self_conjugate' is meant to do there. You want to define IsSelfConjugate as a Prop on YoungDiagram.

[ShaoYu]

Determine whether the Young diagram of a natural number partition of n corresponds to a self-conjugate partition, and then combine the partitions that satisfy this condition into a set.

[ShaoYu]

import Mathlib

open Finset Nat Std List

open Multiset
open BigOperators Partition Nat List
open Function YoungDiagram
def self_conjugate' (n : ℕ) :=
  fun (μ : YoungDiagram) => if μ.cells.card = n ∧ μ.transpose.cells = μ.cells then
    {μ}
  else
    Finset.empty

#check self_conjugate'


def self_conjugate (n : ℕ) (μ : YoungDiagram)  :=
  Finset.univ.filter (fun c => c ∈ (self_conjugate' n μ).erase ∅)

[Kevin Buzzard]

Is this code LLM-generated? I think you'd be better off learning some of the basics first.

[ShaoYu]

No, I wrote this myself. But you’re right—I really need to learn the basics of Lean. Whenever I try to define something new or write my own statements, I don’t know where to start, and I often make mistakes.May you help me solve the mistake?
Thanks.

[Kenny Lau]

@ShaoYu write a function IsSelfConjugate that takes a young diagram and returns a Prop that says it is self conjugate

[ShaoYu]

import Mathlib

open Finset Nat Std List

open Multiset
open BigOperators Partition Nat List
open Function YoungDiagram


def IsSelfConjugate (n : ℕ) (μ : YoungDiagram) :=
  μ.cells.card = n ∧ μ.transpose.cells = μ.cells

instance (n : ℕ) : DecidablePred (IsSelfConjugate n) :=
fun μ =>
  have : Decidable (μ.cells.card = n) :=
    Nat.decEq (Finset.card μ.cells) n
  have : Decidable (μ.transpose.cells = μ.cells) :=
    Finset.decidableEq μ.transpose.cells μ.cells
  inferInstanceAs (Decidable (μ.cells.card = n ∧ μ.transpose.cells = μ.cells))


def self_conjugate'' (n : ℕ) (μ : YoungDiagram):=
   Finset.univ.filter fun μ => IsSelfConjugate n μ

I tried it, but my goal is to prove that the card of partitions into distinct odd parts is equal to the card of self-conjugate partitions, and I encountered the error failed to synthesize Fintype YoungDiagram.

[Kenny Lau]

@ShaoYu your IsSelfConjugate is now more correct. you should always specify the type of the thing you’re defining, which means you should replace := with : Prop :=

also YoungDiagram is not a Fintype because you haven’t restricted n.

[Kenny Lau]

i don’t know what’s the best way to solve this problem right now because i don’t know what the conventions are

[Kenny Lau]

in some sense your definition of IsSelfConjugate is wrong because you included a condition on the cardinality, these should be separate things.

[ShaoYu]

okok,thank you very much,I will continue searching for a solution.