OAI/Geometry/RCD/Coordinates/BilinearHeatEnvelope.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.geometric_causal_sum_succ line 13
2. theorem OAI.RegularPointCoordinates.heat_envelope_le_current line 28

   Source documentation

   The actual geometric source envelope is bounded by the current heat metric under slow growth and small mass. Its finite background is explicit.

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

3. theorem OAI.RegularPointCoordinates.bilinear_heat_comparison_of_envelope line 68

   Source documentation

   Once the signed scalar source estimate is proved, polarization gives exactly the asymmetric bilinear estimate required by the coordinate argument.

   theorem bilinear_heat_comparison_of_envelope (Q F D : E →L[ℝ] E)
       (hF : F.IsPositive) (hD : D.IsSymmetric) {C B : ℝ}
       (hsource : ∀ v, |⟪v, D v⟫_ℝ| ≤ C * ⟪v, F v⟫_ℝ)
       (hcurrent : ∀ v, ⟪v, F v⟫_ℝ ≤ B * ⟪v, Q v⟫_ℝ) (v w : E) :
       ⟪v, D w⟫_ℝ ^ 2 ≤ (C ^ 2 * B) * ⟪v, Q v⟫_ℝ * ⟪w, F w⟫_ℝ := by
   …