SlowHeatGrowth.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Slow growth of the actual heat frames from relative mean comparison

theorem OAI.RegularPointCoordinates.slow_heat_step_of_relative_means line 16

Source documentation

Fixed tolerances small enough for the square-inverse growth in the cumulative heat argument. The comparison is in the original frame.

theorem slow_heat_step_of_relative_means {r s q t : ℝ}
    (hr : 0 ≤ r) (hmean : (1 - (1 / 64 : ℝ)) * r ≤ s)
    (hq : q ≤ (1 + (1 / 64 : ℝ)) * r)
    (ht : (1 - (1 / 64 : ℝ)) * s ≤ t) :
    q ≤ (9 / 8 : ℝ) * t := by
…

theorem OAI.RegularPointCoordinates.geometric_form_growth line 25

Source documentation

Iterating adjacent quadratic comparisons costs an arbitrarily fixed small geometric factor, here 9/8 rather than the coarse factor two.

theorem geometric_form_growth {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    (Q : ℕ → E →L[ℝ] E) {g : ℝ} (hg : 0 ≤ g)
    (hstep : ∀ i v, ⟪v, Q i v⟫_ℝ ≤ g * ⟪v, Q (i + 1) v⟫_ℝ)
    {j i : ℕ} (hji : j ≤ i) (v : E) :
    ⟪v, Q j v⟫_ℝ ≤ g ^ (i - j) * ⟪v, Q i v⟫_ℝ := by
…

theorem OAI.RegularPointCoordinates.inverse_norm_sq_of_slow_growth line 44

Source documentation

A near-identity initial heat Gram and slow growth control every inverse vector. This is the norm hypothesis required by the cumulative comparison.

theorem inverse_norm_sq_of_slow_growth {E : Type*}
    [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    (Q : ℕ → E ≃L[ℝ] E)
    (hstep : ∀ i v, ⟪v, Q i v⟫_ℝ ≤ (9 / 8 : ℝ) * ⟪v, Q (i + 1) v⟫_ℝ)
    (hbase : ∀ v, (1 / 2 : ℝ) * ‖v‖ ^ 2 ≤ ⟪v, Q 0 v⟫_ℝ)
    (i : ℕ) (v : E) :
    ‖(Q i).symm v‖ ^ 2 ≤ 4 * (81 / 64 : ℝ) ^ i * ‖v‖ ^ 2 := by
…

theorem OAI.RegularPointCoordinates.half_decrement_of_slow_step line 78

Source documentation

Slow growth and positivity imply the relatively small decrement used in the inverse-energy telescope.

theorem half_decrement_of_slow_step {E : Type*}
    [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    (Q P : E →L[ℝ] E) (hP : P.IsPositive)
    (hstep : ∀ v, ⟪v, Q v⟫_ℝ ≤ (9 / 8 : ℝ) * ⟪v, P v⟫_ℝ) (v : E) :
    ⟪v, (Q - P) v⟫_ℝ ≤ (1 / 2 : ℝ) * ⟪v, Q v⟫_ℝ := by
…

theorem OAI.RegularPointCoordinates.conjugated_adjacent_heat_step line 88

Source documentation

The slow step for the same original coordinate frame follows from its adjacent mean comparison and the two relative heat comparisons.

theorem conjugated_adjacent_heat_step {X : Type*}
    [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [ProperSpace X]
    {K : ℝ} (m : ℕ) (hX : NoncollapsedRCD K (m + 1) X)
    {a : ℝ} (ha : 0 ≤ a)
    (hBG : BallVolumeComparison (hausdorff (m + 1) X) (comparisonModelVolume m a))
    (u : Fin (m + 1) → SobolevSpace (hausdorff (m + 1) X) hX.quadratic)
    (A S : Euclidean (m + 1) ≃L[ℝ] Euclidean (m + 1))
    {p : X} {r ε : ℝ} {w : X → Euclidean (m + 1)}
    (hr : 0 < r) (hscale : a * (3 * (r / 2)) ≤ 1) (hε : 0 ≤ ε)
    (hsmall : ((m + 1 : ℕ) : ℝ) ^ 2 * (normalizationVolumeRatio m * ε) ≤ 1 / 64)
    (hfirst : FirstOrderSplittingOn (hausdorff (m + 1) X) hX.quadratic p r ε
      (transformedColumn (hausdorff (m + 1) X) hX.quadratic u A) w)
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.normalizationVolumeRatio, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.transformedColumn