HeatCumulative.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Accumulating heat decrements in changing inverse metrics

All forms act on one fixed real inner product space. The hypotheses are local heat envelopes, small one-step decrements, and slow metric growth. In particular, neither the weighted total nor the cumulative comparison is an input.

theorem OAI.RegularPointCoordinates.positive_form_add_le_two line 23

Source documentation

The quadratic-form version of the two-term Young inequality.

theorem positive_form_add_le_two {D : E →L[ℝ] E} (hD : D.IsPositive) (x y : E) :
    ⟪x + y, D (x + y)⟫_ℝ ≤ 2 * ⟪x, D x⟫_ℝ + 2 * ⟪y, D y⟫_ℝ := by
…

theorem OAI.RegularPointCoordinates.inverse_vector_telescopes line 31

Source documentation

Inverse vectors telescope over every finite interval.

theorem inverse_vector_telescopes (Q : ℕ → E ≃L[ℝ] E) (xi : E)
    {j i : ℕ} (hji : j ≤ i) :
    (Q i).symm xi - (Q j).symm xi =
      ∑ l ∈ Finset.Ico j i,
        (((Q (l + 1)).symm : E →L[ℝ] E) - ((Q l).symm : E →L[ℝ] E)) xi := by
…

theorem OAI.RegularPointCoordinates.inverse_vector_interval_energy line 45

Source documentation

Slow growth transports the energy of inverse increments to an earlier metric. The resulting lag factor is precisely the one used in the heat kernel convolution.

theorem inverse_vector_interval_energy (Q : ℕ → E ≃L[ℝ] E)
    (hQ : ∀ i, (Q i : E →L[ℝ] E).IsPositive)
    (hdec : ∀ i, ((Q i : E →L[ℝ] E) - (Q (i + 1) : E →L[ℝ] E)).IsPositive)
    (hsmall : ∀ i v, ⟪v, ((Q i : E →L[ℝ] E) - (Q (i + 1) : E →L[ℝ] E)) v⟫_ℝ ≤
      (1 / 2 : ℝ) * ⟪v, Q i v⟫_ℝ)
    {G g : ℝ} (hG : 0 ≤ G) (hg : 1 ≤ g)
    (hgrowth : ∀ j l, j ≤ l → ∀ v, ⟪v, Q j v⟫_ℝ ≤ G * g ^ (l - j) * ⟪v, Q l v⟫_ℝ)
    (xi : E) {j i : ℕ} (hji : j ≤ i) :
    ⟪(Q i).symm xi - (Q j).symm xi,
      Q j ((Q i).symm xi - (Q j).symm xi)⟫_ℝ ≤
      G * (i - j : ℕ) * g ^ (i - j) *
        ∑ l ∈ Finset.Ico j i,
…

theorem OAI.RegularPointCoordinates.moving_form_convolution_le line 86

Source documentation

Summing a moving-vector convolution introduces only the ordinary geometric constant and the second lag moment.

theorem moving_form_convolution_le (Q N : ℕ → E →L[ℝ] E)
    (hN : ∀ i, (N i).IsPositive) (a : ℕ → E) (b : ℕ → ℝ)
    (hb : ∀ i, 0 ≤ b i) {epsilon beta G g : ℝ}
    (hepsilon : 0 ≤ epsilon) (hbeta : 0 ≤ beta) (hbeta1 : beta < 1)
    (hG : 0 ≤ G) (hg : 0 ≤ g) (hbetag : beta * g < 1)
    (hsmall : ∀ i v, ⟪v, N i v⟫_ℝ ≤ epsilon * ⟪v, Q i v⟫_ℝ)
    (hinterval : ∀ j i, j ≤ i →
      ⟪a i - a j, Q j (a i - a j)⟫_ℝ ≤
        G * (i - j : ℕ) * g ^ (i - j) * ∑ l ∈ Finset.Ico j i, b l)
    (k : ℕ) :
    (∑ i ∈ Finset.range k, ∑ j ∈ Finset.range (i + 1),
      beta ^ (i - j) * ⟪a i, N j (a i)⟫_ℝ) ≤
…

theorem OAI.RegularPointCoordinates.inverse_background_sum_le line 146

Source documentation

A geometric background contribution remains bounded after applying inverse metrics whose squared norms have slower exponential growth.

theorem inverse_background_sum_le (a : ℕ → E) (xi : E)
    {beta g K : ℝ} (hbeta : 0 ≤ beta) (hg : 0 ≤ g) (hK : 0 ≤ K)
    (hbg : beta * g < 1)
    (ha : ∀ i, ‖a i‖ ^ 2 ≤ K * g ^ i * ‖xi‖ ^ 2) (k : ℕ) :
    (∑ i ∈ Finset.range k, beta ^ i * ‖a i‖ ^ 2) ≤
      K * (1 - beta * g)⁻¹ * ‖xi‖ ^ 2 := by
…

theorem OAI.RegularPointCoordinates.inverse_energy_telescopes line 169

Source documentation

Exact scalar telescope of the inverse increments.

theorem inverse_energy_telescopes (Q : ℕ → E ≃L[ℝ] E) (xi : E) (k : ℕ) :
    (∑ i ∈ Finset.range k,
      ⟪xi, (((Q (i + 1)).symm : E →L[ℝ] E) - ((Q i).symm : E →L[ℝ] E)) xi⟫_ℝ) =
      ⟪xi, (Q k).symm xi⟫_ℝ - ⟪xi, (Q 0).symm xi⟫_ℝ := by
…

theorem OAI.RegularPointCoordinates.inverse_heat_envelope_sum_le line 178

Source documentation

The heat envelope implies a weighted total estimate at the moving inverse vectors. This is proved before using either cumulative comparison.

theorem inverse_heat_envelope_sum_le (Q : ℕ → E ≃L[ℝ] E)
    (N F : ℕ → E →L[ℝ] E)
    (hQ : ∀ i, (Q i : E →L[ℝ] E).IsPositive)
    (hN : ∀ i, (N i).IsPositive)
    (hdec : ∀ i, ((Q i : E →L[ℝ] E) - (Q (i + 1) : E →L[ℝ] E)).IsPositive)
    (hsmall : ∀ i v, ⟪v, ((Q i : E →L[ℝ] E) - (Q (i + 1) : E →L[ℝ] E)) v⟫_ℝ ≤
      (1 / 2 : ℝ) * ⟪v, Q i v⟫_ℝ)
    {epsilon beta G g g₀ K : ℝ}
    (hepsilon : 0 ≤ epsilon) (hbeta : 0 ≤ beta) (hbeta1 : beta < 1)
    (hG : 0 ≤ G) (hg : 1 ≤ g) (hbg : beta * g < 1)
    (hg₀ : 0 ≤ g₀) (hK : 0 ≤ K) (hbg₀ : beta * g₀ < 1)
    (hgrowth : ∀ j i, j ≤ i → ∀ v,
…

theorem OAI.RegularPointCoordinates.inverse_heat_cumulative_comparison line 224

Source documentation

The actual central cumulative comparison and weighted heat total follow from the two heat decrement inequalities. The smallness condition absorbs the moving-normalization error; it does not assume a cumulative conclusion.

theorem inverse_heat_cumulative_comparison (Q : ℕ → E ≃L[ℝ] E)
    (N F : ℕ → E →L[ℝ] E)
    (hQ : ∀ i, (Q i : E →L[ℝ] E).IsPositive)
    (hN : ∀ i, (N i).IsPositive)
    (hdec : ∀ i, ((Q i : E →L[ℝ] E) - (Q (i + 1) : E →L[ℝ] E)).IsPositive)
    (hsmall : ∀ i v, ⟪v, ((Q i : E →L[ℝ] E) - (Q (i + 1) : E →L[ℝ] E)) v⟫_ℝ ≤
      (1 / 2 : ℝ) * ⟪v, Q i v⟫_ℝ)
    {epsilon beta G g g₀ K C K₀ : ℝ}
    (hepsilon : 0 ≤ epsilon) (hbeta : 0 ≤ beta) (hbeta1 : beta < 1)
    (hG : 0 ≤ G) (hg : 1 ≤ g) (hbg : beta * g < 1)
    (hg₀ : 0 ≤ g₀) (hK : 0 ≤ K) (hbg₀ : beta * g₀ < 1)
    (hC : 0 ≤ C) (hK₀ : 0 ≤ K₀)
…

theorem OAI.RegularPointCoordinates.enlarged_mass_inverse_sum_le line 331

Source documentation

The lower heat decrement controls all finite families of enlarged mass forms, with the cardinal bound as the only dependence on the family.

theorem enlarged_mass_inverse_sum_le {ι : Type*}
    (Q : ℕ → E ≃L[ℝ] E) (M : ℕ → ι → E →L[ℝ] E) (s : ℕ → Finset ι)
    (hQ : ∀ i, (Q i : E →L[ℝ] E).IsPositive)
    (hdec : ∀ i, ((Q i : E →L[ℝ] E) - (Q (i + 1) : E →L[ℝ] E)).IsPositive)
    (hsmall : ∀ i v, ⟪v, ((Q i : E →L[ℝ] E) - (Q (i + 1) : E →L[ℝ] E)) v⟫_ℝ ≤
      (1 / 2 : ℝ) * ⟪v, Q i v⟫_ℝ)
    {C : ℝ} (hC : 0 ≤ C) (J : ℕ) (hcard : ∀ i, (s i).card ≤ J)
    (hmass : ∀ i y, y ∈ s i → ∀ v, ⟪v, M i y v⟫_ℝ ≤
      C * ⟪v, ((Q i : E →L[ℝ] E) - (Q (i + 1) : E →L[ℝ] E)) v⟫_ℝ)
    (xi : E) (k : ℕ) :
    (∑ i ∈ Finset.range k, ∑ y ∈ s i, ⟪(Q i).symm xi, M i y ((Q i).symm xi)⟫_ℝ) ≤
      (J : ℝ) * C * ⟪xi, (Q k).symm xi⟫_ℝ := by
…