ActualLogMeasureFurther.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.no_eventual_polynomial_exponential_growth line 33

Source comment

The quantifier order in bounds.tex: every finite box has its own eventual index. No common threshold for infinitely many boxes is needed.

theorem no_eventual_polynomial_exponential_growth
    (M : ℕ → ℕ → ℝ) (k l₀ : ℕ) {c q C : ℝ}
    (hc : 0 < c) (hq : 1 < q)
    (hpos : ∀ᶠ j in atTop, c ≤ M j l₀)
    (hstep : ∀ l, l₀ ≤ l → ∀ᶠ j in atTop, q * M j l ≤ M j (l+1))
    (hupper : ∀ L, l₀ ≤ L → ∀ᶠ j in atTop, M j L ≤ C * (L+1:ℝ)^k) : False := by
…

theorem OAI.AffineBernstein.no_eventual_polynomial_shell_growth line 68

Source comment

The source shell inequality has precisely the exponential recurrence required above. Integrals may vary with the approximating index.

theorem no_eventual_polynomial_shell_growth
    (M : ℕ → ℕ → ℝ) (k l₀ : ℕ) {c A C : ℝ}
    (hc : 0 < c) (hA : 0 < A)
    (hpos : ∀ᶠ j in atTop, c ≤ M j l₀)
    (hshell : ∀ l, l₀ ≤ l → ∀ᶠ j in atTop,
      M j l ≤ A * (M j (l+1)-M j l))
    (hupper : ∀ L, l₀ ≤ L → ∀ᶠ j in atTop, M j L ≤ C * (L+1:ℝ)^k) : False := by
…

theorem OAI.AffineBernstein.lipschitzWith_mul_unit line 85

Source comment

A product of two unit-bounded Lipschitz functions has the sum of their Lipschitz constants. Here the multiplication is the ring multiplication on ℝ.

theorem lipschitzWith_mul_unit {X : Type*} [PseudoMetricSpace X]
    {f g : X → ℝ} {K L : NNReal} (hf : LipschitzWith K f) (hg : LipschitzWith L g)
    (hfb : ∀ x, ‖f x‖ ≤ 1) (hgb : ∀ x, ‖g x‖ ≤ 1) :
    LipschitzWith (K+L) (fun x => f x*g x) := by
…

theorem OAI.AffineBernstein.lipschitzWith_prod_unit line 104
theorem OAI.AffineBernstein.smoothTransition_exists_lipschitz line 123
Source comment
The fixed smooth transition has some finite global Lipschitz constant; constancy off [0,1] makes the derivative bound compact.
```
theorem smoothTransition_exists_lipschitz : ∃ K : NNReal, LipschitzWith K Real.smoothTransition := by
…
```
def OAI.AffineBernstein.logarithmicCutoff line 149
Source comment
Closed boxes in the literal logarithmic base coordinates. A fixed-width smooth box cutoff; its derivatives have no dependence on L apart from coordinate translations.
```
def logarithmicCutoff (k : ℕ) (L : ℝ) (x : Space k) : ℝ :=
…
```
Mentions: OAI.AffineBernstein.Space
theorem OAI.AffineBernstein.logarithmicCutoff_mem_Icc line 152
theorem OAI.AffineBernstein.logarithmicCutoff_one line 160
theorem OAI.AffineBernstein.logarithmicCutoff_zero line 169
theorem OAI.AffineBernstein.logarithmicCutoff_smooth line 180
theorem OAI.AffineBernstein.logarithmicCutoff_uniform_lipschitz line 190
Source comment
One constant controls every translated logarithmic cutoff.
```
theorem logarithmicCutoff_uniform_lipschitz (k : ℕ) :
    ∃ K : NNReal, 0 < K ∧ ∀ L : ℝ, LipschitzWith K (logarithmicCutoff k L) := by
…
```
Mentions: OAI.AffineBernstein.logarithmicCutoff
theorem OAI.AffineBernstein.logarithmicBox_mono line 238
theorem OAI.AffineBernstein.logarithmicBox_isClosed line 241
theorem OAI.AffineBernstein.logarithmicBox_isCompact line 247
theorem OAI.AffineBernstein.logarithmicCutoff_hasCompactSupport line 258
theorem OAI.AffineBernstein.logarithmicCutoff_fderiv_eq_zero_of_mem line 267
Source comment
The derivative vanishes on the inner closed box, including its faces.
```
theorem logarithmicCutoff_fderiv_eq_zero_of_mem {k : ℕ} {L : ℝ} {x : Space k}
    (hx : x ∈ logarithmicBox k L) : fderiv ℝ (logarithmicCutoff k L) x = 0 := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.logarithmicBox, OAI.AffineBernstein.logarithmicCutoff
theorem OAI.AffineBernstein.logarithmicCutoff_fderiv_eq_zero_of_outside line 277
Source comment
The same holds at and outside the outer faces; no zero-boundary-mass assumption is needed in the ensuing shell estimate.
```
theorem logarithmicCutoff_fderiv_eq_zero_of_outside {k : ℕ} {L : ℝ} {x : Space k}
    (hx : ∃ i, L+1 ≤ |x i|) : fderiv ℝ (logarithmicCutoff k L) x = 0 := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.logarithmicCutoff

theorem OAI.AffineBernstein.logarithmic_shell_growth line 287

Source comment

The logarithmic Poincaré inequality turns the genuine smooth cutoff into mass growth in a fixed-width shell. Measures need only be finite on this box.

theorem logarithmic_shell_growth {k : ℕ} {L : ℝ} (μ : Measure (Space k))
    {K : NNReal} (hK : LipschitzWith K (logarithmicCutoff k L)) (hfin : μ (logarithmicBox k (L+1)) ≠ ⊤)
    {A : ℝ} (hA : 0 ≤ A)
    (hP : (∫ x, (logarithmicCutoff k L x)^2 ∂μ) ≤
      A * ∫ x, ‖fderiv ℝ (logarithmicCutoff k L) x‖^2 ∂μ) :
    μ.real (logarithmicBox k L) ≤ A*(K:ℝ)^2 *
      (μ.real (logarithmicBox k (L+1))-μ.real (logarithmicBox k L)) := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.logarithmicCutoff, OAI.AffineBernstein.logarithmicBox

theorem OAI.AffineBernstein.no_polynomial_logarithmic_poincare line 364

Source comment

The growth contradiction, for actual Borel measures and actual smooth cutoffs, with only eventual availability on each finite logarithmic box.

theorem no_polynomial_logarithmic_poincare {k l₀ : ℕ} (μ : ℕ → Measure (Space k))
    {c A C : ℝ} (hc : 0 < c) (hA : 0 < A)
    (hpos : ∀ᶠ j in atTop, c ≤ (μ j).real (logarithmicBox k l₀))
    (hfin : ∀ L : ℕ, l₀ ≤ L → ∀ᶠ j in atTop, μ j (logarithmicBox k L) ≠ ⊤)
    (hupper : ∀ L : ℕ, l₀ ≤ L → ∀ᶠ j in atTop,
      (μ j).real (logarithmicBox k L) ≤ C*(L+1:ℝ)^k)
    (hP : ∀ L : ℕ, l₀ ≤ L → ∀ᶠ j in atTop,
      (∫ x, (logarithmicCutoff k L x)^2 ∂μ j) ≤
        A * ∫ x, ‖fderiv ℝ (logarithmicCutoff k L) x‖^2 ∂μ j) : False := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.logarithmicBox, OAI.AffineBernstein.logarithmicCutoff