RebaseWeakening

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

1. The scalar move

theorem Algsuperdiff.Section4.Provider.ExcessDecay.rpow_legMove_le {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) : s.rpow (-(9 / 2)) ≤ s.rpow (-6)

The two leg moves, as one scalar inequality.

rpow_neg_nine_halves_le_rpow_neg_six is exactly this fact; it is re-exported here under a re-base name so that the harmonic lane reads it from its own module rather than through the excess-decay consumer check.

2. The real-valued leg

theorem Algsuperdiff.Section4.Provider.ExcessDecay.rpow_legMove_mul_le {s a T : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (ha : 0 ≤ a) (hT : 0 ≤ T) : s.rpow (-(9 / 2)) * a * T ≤ s.rpow (-6) * a * T

One leg of a real-valued clause, moved. The leg's shape is the one every proved transcription uses: the s-power, then a nonnegative 3-power, then the toReal of an ℝ≥0∞ seminorm.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.realBracket_legMove_le {C s a₄ a₅ T₄ T₅ H : ℝ} (hC : 0 ≤ C) (hs : 0 < s) (hs1 : s ≤ 1) (h₄ : 0 ≤ a₄) (h₅ : 0 ≤ a₅) (hT₄ : 0 ≤ T₄) (hT₅ : 0 ≤ T₅) : C * (H + s.rpow (-(9 / 2)) * a₄ * T₄ + s.rpow (-(9 / 2)) * a₅ * T₅) ≤ C * (H + s.rpow (-6) * a₄ * T₄ + s.rpow (-6) * a₅ * T₅)

The real-valued display, with both ∇h legs moved to s^{-6}.

H carries the two untouched summands (the flux bracket and the σ force leg); the two ∇h legs move. Abstract in every carrier, so this one lemma re-cuts each …Real clause of the lane.

3. The ℝ≥0∞ prefactor product