OAI/Analysis/HenonEmden/LayerRecovery.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HenonLaneEmden.WeightedLayers.source_root line 9
2. lemma OAI.HenonLaneEmden.WeightedLayers.weighted_layer_identity line 15
3. lemma OAI.HenonLaneEmden.WeightedLayers.layer_root_bounds line 41
4. lemma OAI.HenonLaneEmden.WeightedLayers.pressure_recovery_pointwise line 53

   Source documentation

   The exact scalar recovery inequality before integration.

   lemma pressure_recovery_pointwise {h χ u τ endpoint error : ℝ}
       (hχ : 0 ≤ χ) (hχh : χ ≤ h) (hτ : 0 ≤ τ)
       (hend : |endpoint-τ| ≤ error*u) :
       h*(u-τ)-χ*(u-endpoint) ≤ (h-χ)*u+error*h*u := by
   …