OAI/Probability/InvariantIsing/Fields/FieldParameterGrowth.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local uniform growth follows from the actual bounded spatial derivative and continuity of the parameter at spatial coordinate zero.

  1. lemma OAI.InvariantIsing.field_spatial_linearGrowth line 14
  2. lemma OAI.InvariantIsing.field_parameter_growth_eventually line 31