`corePairStretchFactor_pos`

proved

show as: view math explainer →

module: IndisputableMonolith.NavierStokes.DiscreteNSOperator
domain: NavierStokes
line: 155 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NavierStokes.DiscreteNSOperator on GitHub at line 155.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 152    (i : Fin siteCount) : ℝ :=
 153  1 + op.dt * velocityGradientMag op.topology op.h op.velocity i
 154
 155theorem corePairStretchFactor_pos {siteCount : ℕ} (op : CoreNSOperator siteCount)
 156    (i : Fin siteCount) : 0 < corePairStretchFactor op i := by
 157  unfold corePairStretchFactor
 158  linarith [mul_nonneg op.dt_pos.le (op.gradientMag_nonneg i)]
 159
 160/-- The derived pair event at each site. -/
 161def corePairEvent {siteCount : ℕ} (op : CoreNSOperator siteCount)
 162    (i : Fin siteCount) : PairEvent where
 163  amplitude := corePairAmplitude op i
 164  stretchFactor := corePairStretchFactor op i
 165  amplitude_pos := corePairAmplitude_pos op i
 166  stretchFactor_pos := corePairStretchFactor_pos op i
 167
 168/-- The stretching bound from the core operator matches the pairwise change
 169because both sides use the same amplitude and stretch factor. -/
 170theorem core_stretching_le_pair_budget {siteCount : ℕ}
 171    (op : CoreNSOperator siteCount) (i : Fin siteCount) :
 172    op.contributions.stretching i ≤
 173      pairwiseStretchingChange (corePairAmplitude op i) (corePairStretchFactor op i) := by
 174  unfold pairwiseStretchingChange corePairAmplitude corePairStretchFactor
 175  exact op.stretching_bound i
 176
 177/-- Total derived pair budget from the core. -/
 178def coreOperatorPairBudget {siteCount : ℕ} (op : CoreNSOperator siteCount) : ℝ :=
 179  indexedPairBudget (corePairEvent op)
 180
 181theorem coreOperatorPairBudget_nonneg {siteCount : ℕ}
 182    (op : CoreNSOperator siteCount) :
 183    0 ≤ coreOperatorPairBudget op :=
 184  indexedPairBudget_nonneg (corePairEvent op)
 185

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.