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

matrixNeumannStub

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)

  48noncomputable def matrixNeumannStub : MatrixNeumannFacts where
  49  higher_terms_bound := by

proof body

Definition body.

  50    intro g0 h h_small x μ ν
  51    have : |(0 : ℝ)| ≤ 16 * (0.1 : ℝ) ^ 2 := by norm_num
  52    simpa using this
  53
  54instance : MatrixNeumannFacts := matrixNeumannStub
  55
  56-- FibonacciFacts instance now provided constructively in Verification/Necessity/PhiNecessity.lean
  57
  58-- KolmogorovFacts now has a real instance in Verification/Necessity/DiscreteNecessity.lean
  59-- based on algorithmic information theory axiom
  60

depends on (1)

Lean names referenced from this declaration's body.