lemma proved term proof

`OSPositivity_default`

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

formal statement (Lean)

  33lemma OSPositivity_default (_μ : LatticeMeasure) : OSPositivity _μ := by

proof body

Term-mode proof.

  34  refine ⟨default, 1, ?_⟩
  35  dsimp [OverlapLowerBoundOS]
  36  constructor <;> norm_num
  37
  38/-- Overlap lower bound for a kernel (β ∈ (0,1]). -/

depends on (8)

Lean names referenced from this declaration's body.

default in IndisputableMonolith.Chemistry.PeriodicTable decl_use
default in IndisputableMonolith.Config.Flags decl_use
kernel in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
kernel in IndisputableMonolith.ILG.Kernel decl_use
LatticeMeasure in IndisputableMonolith.YM.OS decl_use
OSPositivity in IndisputableMonolith.YM.OS decl_use
OverlapLowerBoundOS in IndisputableMonolith.YM.OS decl_use