corePairEvent

formal source

 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
 186/-- The derived pair budget is absorbed by viscosity. -/
 187theorem core_pair_budget_absorbed {siteCount : ℕ}
 188    (op : CoreNSOperator siteCount) :
 189    coreOperatorPairBudget op ≤ - totalViscous op.contributions := by
 190  unfold coreOperatorPairBudget indexedPairBudget total
 191  simp only [corePairEvent, pairEventBudget, corePairAmplitude, corePairStretchFactor]