EventualEnvelopeOrder.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Pointwise envelope order after the finite initial scales

theorem OAI.RegularPointCoordinates.EventualHeatControls.envelope_le_current line 17

Source documentation

The actual eventual heat controls also give order of the mass envelope by the current metric, with the finite background kept explicit.

theorem EventualHeatControls.envelope_le_current
    {Q : ℕ → E ≃L[ℝ] E} {N F : ℕ → E →L[ℝ] E} {J : ℕ} {ε C b T : ℝ}
    (h : EventualHeatControls Q N F J ε C)
    (hQ : ∀ i, (Q i : E →L[ℝ] E).IsPositive)
    (hε : 0 ≤ ε) (hb : 0 ≤ b) (hT : 0 ≤ T)
    (hbase : ∀ v, ‖v‖ ^ 2 ≤ T * ⟪v, Q J v⟫_ℝ)
    (hbackground : ∀ i v, ⟪v, F (J + i) v⟫_ℝ ≤ b * (3 / 4 : ℝ) ^ i * ‖v‖ ^ 2 +
      ∑ j ∈ Finset.range (i + 1), (3 / 4 : ℝ) ^ (i - j) * ⟪v, N (J + j) v⟫_ℝ)
    (i : ℕ) (v : E) :
    ⟪v, F (J + i) v⟫_ℝ ≤ (b * T + 8 * ε) * ⟪v, Q (J + i) v⟫_ℝ := by
…

Mentions: OAI.RegularPointCoordinates.EventualHeatControls