matrixNeumannStub

formal source

  45
  46instance : LandauCompositionFacts := landauFactsStub
  47
  48noncomputable def matrixNeumannStub : MatrixNeumannFacts where
  49  higher_terms_bound := by
  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
  61noncomputable def linearizedPDEStub : LinearizedPDEFacts where
  62  solution_exists := by
  63    intro ng ρ m_squared
  64    refine ⟨{ δψ := fun _ => 0, small := by intro _ _; norm_num }, ?_, ?_⟩
  65    · intro x; simp [Linearized00Equation]
  66    · refine ⟨⟨fun _ => 1, by intro; simp⟩, fun _ => rfl, rfl⟩
  67  remainder_order := by
  68    intro ng δψ ρ ε
  69    refine ⟨fun _ => |ε|, ?_, ?_⟩
  70    · intro; exact ⟨by norm_num, by intro; norm_num⟩
  71    · intro x; simp [IsOrderEpsilonSquared, abs_mul]
  72
  73instance : LinearizedPDEFacts := linearizedPDEStub
  74
  75noncomputable def ppnInverseStub : PPNInverseFacts where
  76  inverse_approx := by
  77    intro pots params x μ ρ
  78    simpa using show |(0 : ℝ)| < 0.001 by norm_num