matrixBridgeFactsStub

formal source

  34
  35instance : CurvatureExpansionFacts := curvatureFactsStub
  36
  37noncomputable def matrixBridgeFactsStub : MatrixBridgeFacts where
  38  weak_field_bound := by intro ctrl ε hbound hε hε'; exact hbound
  39  derivative_bound := by intro ctrl ε hbound hε; trivial
  40
  41instance : MatrixBridgeFacts := matrixBridgeFactsStub
  42
  43noncomputable def landauFactsStub : LandauCompositionFacts where
  44  bigO_comp_continuous := by intro f g h a hf; exact hf
  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