Documentation

LeanPool.HighContrastHomogenization.Support.HighContrast.EntryScale.Basic

Coarse-graining support: Support.HighContrast.EntryScale.Basic #

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Basic metadata for the entry-scale assembly #

This file contains only source-control metadata for the development. Mathematical theorem statements should be introduced only after their source labels and dependency role are recorded.

source
structure HCPolySupport.HighContrast.EntryScale.SourceLabel :
Type

A stable label referencing a statement in the source document.

  • file : String

    The identifier of the source document containing the referenced statement.

  • label : String

    The statement label within the source document.

  • line : Nat

    The line number of the referenced statement in the source document.

Instances For
    source
    def HCPolySupport.HighContrast.EntryScale.instDecidableEqSourceLabel.decEq (x✝ x✝¹ : SourceLabel) :
    Decidable (x✝ = x✝¹)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance HCPolySupport.HighContrast.EntryScale.instDecidableEqSourceLabel :
      DecidableEq SourceLabel
      Equations
      source
      @[instance_reducible]
      instance HCPolySupport.HighContrast.EntryScale.instReprSourceLabel :
      Repr SourceLabel
      Equations
      source
      def HCPolySupport.HighContrast.EntryScale.instReprSourceLabel.repr :
      SourceLabel → Nat → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def HCPolySupport.HighContrast.EntryScale.SourceLabel.highMomentPaper (label : String) (line : Nat) :
        SourceLabel

        A label from the high-moment paper (Armstrong–Kuusi–Loher, to appear).

        Equations
        Instances For