pith. machine review for the scientific record. sign in
structure definition def or abbrev

AbsorptionClassImpossibleHypothesis

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 910structure AbsorptionClassImpossibleHypothesis (AbsorptionClass : ℝ → ℝ → Prop) : Prop where
 911  impossible :
 912    ∀ (η ε0 : ℝ),
 913      0 < η →
 914        0 < ε0 →
 915          ∃ r0 : ℝ,
 916            0 < r0 ∧
 917              ∀ r : ℝ, 0 < r → r ≤ r0 → AbsorptionClass ε0 r → False
 918
 919/-- **Concavity/peak channel elimination (spec layer):** the concavity event cannot occur below some scale.
 920
 921This is the abstract way to “kill (P3)” if it is not already absorbed into `payXi`/`payRho`. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.