OAI/Analysis/FourierLLogL/Thermal/Bias.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Extracting the biased spectrum

  1. def OAI.FourierLLogL.Dyadic.Thermal.ball line 16
  2. lemma OAI.FourierLLogL.Dyadic.Thermal.mem_ball line 18
  3. def OAI.FourierLLogL.Dyadic.Thermal.fnear line 20
  4. def OAI.FourierLLogL.Dyadic.Thermal.separated line 23
  5. def OAI.FourierLLogL.Dyadic.Thermal.request line 27
  6. def OAI.FourierLLogL.Dyadic.Thermal.biases line 32

    Source documentation

    Bias tagged to subgroup characters χ_gx, side coordinate and the fixed child.

    def biases (P : Law (Grid M)) (p : Node) (A : Form M) (hl : l ≤ M)
    (s : Finset (Grid l)) (B : Bool) (v : Grid l → Grid M → ℂ) (β : ℝ) :=
…

    Mentions: OAI.FourierLLogL.Law, OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.Node, OAI.FourierLLogL.Dyadic.Thermal.Form

  7. lemma OAI.FourierLLogL.Dyadic.Thermal.nearby_bias line 39
  8. lemma OAI.FourierLLogL.Dyadic.Thermal.extract_spectrum line 88