Carleson/ToMathlib/Analysis/Fourier/AddCircle.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. theorem fourier_comp_equivAddCircle line 8 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, Fact, LT.lt, OfNat.ofNat, AddCircle, Int, Eq, Complex, ContinuousMap, AddSubgroup.zmultiples, fourier, AddEquiv, AddCircle.equivAddCircle, LT.lt.ne', Fact.out

    Proof uses: Eq.mpr, Subtype, Membership.mem, Submonoid, Submonoid.unitSphere, AddCircle.toCircle, HSMul.hSMul, id, HPow.hPow, Circle, congrArg, AddCircle.toCircle_zsmul, HPow, Eq.rec, Eq.refl, HMul.hMul, Set, Set.Ico, HAdd.hAdd, Equiv and 93 more

    158 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

    Open to load the checked before-and-after goal states.

  2. theorem fourierCoeff_comp_equivAddCircle line 21 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, Fact, LT.lt, OfNat.ofNat, AddCircle, Complex, Int, Eq, fourierCoeff, AddEquiv, AddSubgroup.zmultiples, AddCircle.equivAddCircle, LT.lt.ne', Fact.out

    Proof uses: id, MeasureTheory.integral, AddCircle.haarAddCircle, HSMul.hSMul, ContinuousMap, fourier, Neg.neg, Eq.mpr, HMul.hMul, congrFun', congrArg, funext, Eq.symm, fourier_comp_equivAddCircle, MeasureTheory.MeasurePreserving.integral_comp, AddCircle.measurePreserving_equivAddCircle, Homeomorph.measurableEmbedding, AddCircle.homeomorphAddCircle

    101 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

    Open to load the checked before-and-after goal states.