Mathlib.Analysis.Parametric­Rational­Integral­Analyticity

Analyticity infrastructure for finite-measure integrals with polynomial parameter numerators and affine denominators uniformly separated from zero, including geometric expansions and a scalar interval example.

Definitions 2 core · 0 supporting This file defines the affine denominator and fixed-degree polynomial numerator used by the parametric rational-integral analyticity API.

Building blocks for parametric rational integrals

This file defines the affine denominator and fixed-degree polynomial numerator used by the parametric rational-integral analyticity API.

def affineDenominator reviewed
Causalean.Mathlib.Analysis.ParametricRationalIntegralAnalyticity

Given two real-valued functions, a parameter, and an input point, the affine denominator is given by their displayed linear interpolation at that parameter.

Definition (Lean source)
parameters
α :
Type*
a b :
α → ℝ
t :
ℝ
x :
α
def
affineDenominator a b t x :
ℝ
given by
(1 - t) * a x + t * b x
Causalean.Mathlib.Analysis.ParametricRationalIntegralAnalyticity.affineDenominator · Causalean/Mathlib/Analysis/ParametricRationalIntegralAnalyticity/Definitions.lean:13
def polynomialNumerator reviewed
Causalean.Mathlib.Analysis.ParametricRationalIntegralAnalyticity

Given a degree bound, coefficient functions, a parameter, and an input point, the polynomial numerator is given by the displayed finite polynomial evaluated at that parameter and point.

Definition (Lean source)
parameters
α :
Type*
N :
ℕ
c :
Fin (N + 1) → α → ℝ
t :
ℝ
x :
α
def
polynomialNumerator N c t x :
ℝ
given by
∑ i, c i x * t ^ (i : ℕ)
Causalean.Mathlib.Analysis.ParametricRationalIntegralAnalyticity.polynomialNumerator · Causalean/Mathlib/Analysis/ParametricRationalIntegralAnalyticity/Definitions.lean:18
Affine 1 core · 4 supporting This file proves the elementary uniform-neighborhood and geometric-series facts used to control an affine denominator. ★ affineDenominator_reciprocal_eq_tsum

Uniform control and geometric expansion of affine reciprocals

This file proves the elementary uniform-neighborhood and geometric-series facts used to control an affine denominator. These results contain no measure theory.

theorem affineDenominator_reciprocal_eq_tsum reviewed
Causalean.Mathlib.Analysis.ParametricRationalIntegralAnalyticity

If the affine denominator at the expansion center is nonzero and the normalized affine perturbation has absolute value below one, then the reciprocal affine denominator equals its centered geometric power series.

Formal statement
hypotheses
α :
Type*
α → ℝ
t t₀ :
ℝ
x :
α
hden :
affineDenominator a b t₀ x ≠ 0
hsmall :
|(t - t₀) * (b x - a x) / affineDenominator a b t₀ x| < 1
conclusion
(affineDenominator a b t x)⁻¹
= ∑' n : ℕ, ((-(b x - a x) / affineDenominator a b t₀ x) ^ n / affineDenominator a b t₀ x) * (t - t₀) ^ n
Proof (Lean source)
theorem affineDenominator_reciprocal_eq_tsum {α : Type*} {a b : α → ℝ} {t t₀ : ℝ} {x : α} (hden : affineDenominator a b t₀ x ≠ 0) (hsmall : |(t - t₀) * (b x - a x) / affineDenominator a b t₀ x| < 1) : (affineDenominator a b t x)⁻¹ = ∑' n : ℕ, ((-(b x - a x) / affineDenominator a b t₀ x) ^ n / affineDenominator a b t₀ x) * (t - t₀) ^ n := by let d₀ := affineDenominator a b t₀ x let q := (-(b x - a x) / d₀) * (t - t₀) have hd₀ : d₀ ≠ 0 := hden have hq : |q| < 1 := by have hqeq : q = -((t - t₀) * (b x - a x) / d₀) := by dsimp [q] ring rw [hqeq, abs_neg] exact hsmall have hdiff : affineDenominator a b t x = d₀ + (t - t₀) * (b x - a x) := by dsimp [d₀] simp only [affineDenominator] ring have haff : affineDenominator a b t x = d₀ * (1 - q) := by rw [hdiff] dsimp [q] field_simp ring calc (affineDenominator a b t x)⁻¹ = (d₀ * (1 - q))⁻¹ := by rw [haff] _ = d₀⁻¹ * (1 - q)⁻¹ := by rw [mul_inv] _ = d₀⁻¹ * ∑' n : ℕ, q ^ n := by rw [tsum_geometric_of_abs_lt_one hq] _ = ∑' n : ℕ, d₀⁻¹ * q ^ n := by rw [tsum_mul_left] _ = ∑' n : ℕ, ((-(b x - a x) / affineDenominator a b t₀ x) ^ n / affineDenominator a b t₀ x) * (t - t₀) ^ n := by apply tsum_congr intro n dsimp [d₀, q] rw [mul_pow] simp only [div_eq_mul_inv] ring
Causalean.Mathlib.Analysis.ParametricRationalIntegralAnalyticity.affineDenominator_reciprocal_eq_tsum · Causalean/Mathlib/Analysis/ParametricRationalIntegralAnalyticity/Affine.lean:177 · uses affineDenominator
4 supporting declarations (lemmas, instances)
  • affineDenominator_uniformly_nonzero_near theorem — If the separation margin is positive, the slope bound is nonnegative, the affine denominator is separated from zero at the reference parameter, and its slope is uniformly bounded on the integration set, then it remains separated from zero by half that margin on an explicit parameter neighborhood.
    hypotheses
    α :
    Type*
    Set α
    α → ℝ
    t₀ ε L :
    ℝ
    hε :
    0 < ε
    hL :
    0 ≤ L
    hden :
    ∀ x ∈ K, ε ≤ |affineDenominator a b t₀ x|
    hslope :
    ∀ x ∈ K, |b x - a x| ≤ L
    conclusion
    ∃ r > 0, ∀ t, |t - t₀| < r → ∀ x ∈ K, ε / 2 ≤ |affineDenominator a b t x|
    Proof (Lean source)
    theorem affineDenominator_uniformly_nonzero_near {α : Type*} {K : Set α} {a b : α → ℝ} {t₀ ε L : ℝ} (hε : 0 < ε) (hL : 0 ≤ L) (hden : ∀ x ∈ K, ε ≤ |affineDenominator a b t₀ x|) (hslope : ∀ x ∈ K, |b x - a x| ≤ L) : ∃ r > 0, ∀ t, |t - t₀| < r → ∀ x ∈ K, ε / 2 ≤ |affineDenominator a b t x| := by refine ⟨ε / (2 * (L + 1)), ?_, ?_⟩ · positivity · intro t ht x hx have hL1 : 0 < L + 1 := by linarith have hpert : |(t - t₀) * (b x - a x)| < ε / 2 := by rw [abs_mul] calc |t - t₀| * |b x - a x| ≤ |t - t₀| * L := mul_le_mul_of_nonneg_left (hslope x hx) (abs_nonneg _) _ ≤ |t - t₀| * (L + 1) := by gcongr linarith _ < (ε / (2 * (L + 1))) * (L + 1) := mul_lt_mul_of_pos_right ht hL1 _ = ε / 2 := by field_simp have haff : affineDenominator a b t x = affineDenominator a b t₀ x + (t - t₀) * (b x - a x) := by simp only [affineDenominator] ring have htri : |affineDenominator a b t₀ x| ≤ |affineDenominator a b t x| + |(t - t₀) * (b x - a x)| := by calc |affineDenominator a b t₀ x| = |affineDenominator a b t x - (t - t₀) * (b x - a x)| := by congr 1 rw [haff] ring _ ≤ _ := abs_sub _ _ linarith [hden x hx]
    Causalean.Mathlib.Analysis.ParametricRationalIntegralAnalyticity.affineDenominator_uniformly_nonzero_near · Causalean/Mathlib/Analysis/ParametricRationalIntegralAnalyticity/Affine.lean:15
  • affineDenominator_uniformly_nonzero_on_open_near theorem — If the parameter set is open, the separation margin is positive, the affine denominator is uniformly separated from zero throughout that set and the integration set, and the reference parameter lies in the open set, then some positive ball around it stays in the parameter set and retains the same uniform separation.
    hypotheses
    α :
    Type*
    Set α
    α → ℝ
    O :
    Set ℝ
    ε :
    ℝ
    hO :
    IsOpen O
    hε :
    0 < ε
    hden :
    ∀ t ∈ O, ∀ x ∈ K, ε ≤ |affineDenominator a b t x|
    t₀ :
    ℝ
    ht₀ :
    t₀ ∈ O
    conclusion
    ∃ r > 0,
    Metric.ball t₀ r ⊆ O
    conclusion 1
    t ∈ Metric.ball t₀ r :
    x ∈ K :
    ε ≤ |affineDenominator a b t x|
    Proof (Lean source)
    theorem affineDenominator_uniformly_nonzero_on_open_near {α : Type*} {K : Set α} {a b : α → ℝ} {O : Set ℝ} {ε : ℝ} (hO : IsOpen O) (hε : 0 < ε) (hden : ∀ t ∈ O, ∀ x ∈ K, ε ≤ |affineDenominator a b t x|) {t₀ : ℝ} (ht₀ : t₀ ∈ O) : ∃ r > 0, ball t₀ r ⊆ O ∧ ∀ t ∈ ball t₀ r, ∀ x ∈ K, ε ≤ |affineDenominator a b t x| := by rcases Metric.mem_nhds_iff.mp (hO.mem_nhds ht₀) with ⟨r, hr, hball⟩ exact ⟨r, hr, hball, fun t ht x hx => hden t (hball ht) x hx⟩
    Causalean.Mathlib.Analysis.ParametricRationalIntegralAnalyticity.affineDenominator_uniformly_nonzero_on_open_near · Causalean/Mathlib/Analysis/ParametricRationalIntegralAnalyticity/Affine.lean:56
  • affineDenominator_slope_div_le_inv_radius theorem — If the parameter-ball radius and separation margin are positive and the affine denominator is uniformly separated from zero throughout that ball and the integration set, then the affine slope divided by its central denominator is bounded by the reciprocal radius.
    hypotheses
    α :
    Type*
    Set α
    α → ℝ
    t₀ ε r :
    ℝ
    hr :
    0 < r
    hε :
    0 < ε
    hden :
    ∀ t
    if
    |t - t₀| < r
    then
    ∀ x ∈ K, ε ≤ |affineDenominator a b t x|
    x ∈ K :
    conclusion
    |(b x - a x) / affineDenominator a b t₀ x| ≤ r⁻¹
    Proof (Lean source)
    theorem affineDenominator_slope_div_le_inv_radius {α : Type*} {K : Set α} {a b : α → ℝ} {t₀ ε r : ℝ} (hr : 0 < r) (hε : 0 < ε) (hden : ∀ t, |t - t₀| < r → ∀ x ∈ K, ε ≤ |affineDenominator a b t x|) : ∀ x ∈ K, |(b x - a x) / affineDenominator a b t₀ x| ≤ r⁻¹ := by intro x hx let d₀ := affineDenominator a b t₀ x let s := b x - a x have hd₀_lower : ε ≤ |d₀| := by simpa [d₀] using hden t₀ (by simp [hr]) x hx have hd₀ : d₀ ≠ 0 := by intro hd₀_zero rw [hd₀_zero, abs_zero] at hd₀_lower linarith by_contra hle have hgt : r⁻¹ < |s / d₀| := by simpa [s, d₀] using lt_of_not_ge hle have hs : s ≠ 0 := by intro hs_zero simp [hs_zero] at hgt linarith have hd₀_abs_pos : 0 < |d₀| := abs_pos.mpr hd₀ have hs_abs_pos : 0 < |s| := abs_pos.mpr hs have hcross : |d₀| < r * |s| := by rw [inv_eq_one_div, abs_div] at hgt have h := (div_lt_div_iff₀ hr hd₀_abs_pos).mp hgt nlinarith let t := t₀ - d₀ / s have ht : |t - t₀| < r := by dsimp [t] rw [sub_sub_cancel_left, abs_neg, abs_div] exact (div_lt_iff₀ hs_abs_pos).2 hcross have haff : affineDenominator a b t x = d₀ + (t - t₀) * s := by dsimp [d₀, s] simp only [affineDenominator] ring have hzero : affineDenominator a b t x = 0 := by rw [haff] dsimp [t] field_simp [hs] ring have hpositive := hden t ht x hx rw [hzero, abs_zero] at hpositive linarith
    Causalean.Mathlib.Analysis.ParametricRationalIntegralAnalyticity.affineDenominator_slope_div_le_inv_radius · Causalean/Mathlib/Analysis/ParametricRationalIntegralAnalyticity/Affine.lean:68
  • affineDenominator_uniformly_nonzero_near_of_slope_div_bound theorem — If the separation margin is positive, the relative-slope bound is nonnegative, the central affine denominator is uniformly separated from zero, and the slope-to-denominator ratio is uniformly bounded, then the denominator remains separated by half the margin on an explicit parameter neighborhood.
    hypotheses
    α :
    Type*
    Set α
    α → ℝ
    t₀ ε Q :
    ℝ
    hε :
    0 < ε
    hQ :
    0 ≤ Q
    hden :
    ∀ x ∈ K, ε ≤ |affineDenominator a b t₀ x|
    hratio :
    ∀ x ∈ K, |(b x - a x) / affineDenominator a b t₀ x| ≤ Q
    conclusion
    ∃ r > 0, ∀ t, |t - t₀| < r → ∀ x ∈ K, ε / 2 ≤ |affineDenominator a b t x|
    Proof (Lean source)
    theorem affineDenominator_uniformly_nonzero_near_of_slope_div_bound {α : Type*} {K : Set α} {a b : α → ℝ} {t₀ ε Q : ℝ} (hε : 0 < ε) (hQ : 0 ≤ Q) (hden : ∀ x ∈ K, ε ≤ |affineDenominator a b t₀ x|) (hratio : ∀ x ∈ K, |(b x - a x) / affineDenominator a b t₀ x| ≤ Q) : ∃ r > 0, ∀ t, |t - t₀| < r → ∀ x ∈ K, ε / 2 ≤ |affineDenominator a b t x| := by refine ⟨1 / (2 * (Q + 1)), by positivity, ?_⟩ intro t ht x hx let d₀ := affineDenominator a b t₀ x let s := b x - a x have hd₀_lower : ε ≤ |d₀| := by simpa [d₀] using hden x hx have hd₀ : d₀ ≠ 0 := by intro hd₀_zero rw [hd₀_zero, abs_zero] at hd₀_lower linarith have hQ1 : 0 < Q + 1 := by linarith have hrel : |t - t₀| * |s / d₀| < 1 / 2 := by calc |t - t₀| * |s / d₀| ≤ |t - t₀| * Q := mul_le_mul_of_nonneg_left (by simpa [s, d₀] using hratio x hx) (abs_nonneg _) _ ≤ |t - t₀| * (Q + 1) := by gcongr linarith _ < (1 / (2 * (Q + 1))) * (Q + 1) := mul_lt_mul_of_pos_right ht hQ1 _ = 1 / 2 := by field_simp have hs_factor : |s| = |s / d₀| * |d₀| := by calc |s| = |(s / d₀) * d₀| := by congr 1 field_simp _ = |s / d₀| * |d₀| := abs_mul _ _ have hpert : |(t - t₀) * s| < |d₀| / 2 := by calc |(t - t₀) * s| = (|t - t₀| * |s / d₀|) * |d₀| := by rw [abs_mul, hs_factor] ring _ < (1 / 2) * |d₀| := mul_lt_mul_of_pos_right hrel (abs_pos.mpr hd₀) _ = |d₀| / 2 := by ring have haff : affineDenominator a b t x = d₀ + (t - t₀) * s := by dsimp [d₀, s] simp only [affineDenominator] ring have htri : |d₀| ≤ |affineDenominator a b t x| + |(t - t₀) * s| := by calc |d₀| = |affineDenominator a b t x - (t - t₀) * s| := by congr 1 rw [haff] ring _ ≤ _ := abs_sub _ _ linarith
    Causalean.Mathlib.Analysis.ParametricRationalIntegralAnalyticity.affineDenominator_uniformly_nonzero_near_of_slope_div_bound · Causalean/Mathlib/Analysis/ParametricRationalIntegralAnalyticity/Affine.lean:117
Examples 1 core · 0 supporting This file verifies the API on a scalar integral over a compact real interval. ★ analyticOnNhd_integral_one_add_tx_div_two_add_tx

Examples of polynomial-over-affine integral analyticity

This file verifies the API on a scalar integral over a compact real interval.

theorem analyticOnNhd_integral_one_add_tx_div_two_add_tx reviewed
Causalean.Mathlib.Analysis.ParametricRationalIntegralAnalyticity

The scalar integral of one plus the parameter times the integration variable, divided by two plus that product, is real analytic on the open interval from minus one to one.

Formal statement
conclusion
AnalyticOnNhd ℝ (fun t : ℝ ↦ ∫ x in Icc (0 : ℝ) 1, (1 + t * x) / (2 + t * x)) (Ioo (-1 : ℝ) 1)
Proof (Lean source)
theorem analyticOnNhd_integral_one_add_tx_div_two_add_tx : AnalyticOnNhd ℝ (fun t : ℝ ↦ ∫ x in Icc (0 : ℝ) 1, (1 + t * x) / (2 + t * x)) (Ioo (-1 : ℝ) 1) := by let c : Fin 2 → ℝ → ℝ := fun i x ↦ if i = 0 then 1 else x have h := @analyticOnNhd_setIntegral_polynomial_div_affine ℝ measurableSpace volume (Icc (0 : ℝ) 1) measurableSet_Icc measure_Icc_lt_top.ne 1 c (fun _ ↦ 2) (fun x ↦ 2 + x) (Ioo (-1 : ℝ) 1) 1 1 (fun _ ↦ 1) isOpen_Ioo (by norm_num) (by norm_num) (by intro i fin_cases i · simp [c] · change Measurable (fun x : ℝ ↦ x) fun_prop) (by fun_prop) (by fun_prop) (by intro i x hx fin_cases i · norm_num [c] · simpa [c, abs_of_nonneg hx.1] using hx.2) (by intro x hx simpa [abs_of_nonneg hx.1] using hx.2) (by intro t ht x hx have htx : -1 < t * x := by by_cases ht0 : 0 ≤ t · exact (by norm_num : (-1 : ℝ) < 0).trans_le (mul_nonneg ht0 hx.1) · have htle : t ≤ t * x := by have hmul := mul_le_mul_of_nonpos_left hx.2 (le_of_not_ge ht0) simpa using hmul exact ht.1.trans_le htle have hsep : 1 ≤ 2 + t * x := by linarith rw [show affineDenominator (fun _ : ℝ ↦ 2) (fun x ↦ 2 + x) t x = 2 + t * x by unfold affineDenominator ring] exact hsep.trans (le_abs_self _)) have hfun : (fun t : ℝ ↦ ∫ x in Icc (0 : ℝ) 1, polynomialNumerator 1 c t x / affineDenominator (fun _ : ℝ ↦ 2) (fun x ↦ 2 + x) t x) = (fun t : ℝ ↦ ∫ x in Icc (0 : ℝ) 1, (1 + t * x) / (2 + t * x)) := by funext t apply setIntegral_congr_fun measurableSet_Icc intro x hx dsimp rw [show polynomialNumerator 1 c t x = 1 + t * x by simp [polynomialNumerator, c, Finset.univ_fin2] ring] rw [show affineDenominator (fun _ : ℝ ↦ 2) (fun x ↦ 2 + x) t x = 2 + t * x by unfold affineDenominator ring] rw [hfun] at h exact h
Causalean.Mathlib.Analysis.ParametricRationalIntegralAnalyticity.analyticOnNhd_integral_one_add_tx_div_two_add_tx · Causalean/Mathlib/Analysis/ParametricRationalIntegralAnalyticity/Examples.lean:14
Main 1 core · 4 supporting This file specializes dominated power-series integration to finite-degree polynomial numerators and affine denominators. ★ analyticOnNhd_setIntegral_polynomial_div_affine_of_uniform_nonzero

Analyticity of polynomial-over-affine parameter integrals

This file specializes dominated power-series integration to finite-degree polynomial numerators and affine denominators. The integration set need only have finite measure, so compact sets under a locally finite measure are an important special case.

theorem analyticOnNhd_setIntegral_polynomial_div_affine_of_uniform_nonzero reviewed
Causalean.Mathlib.Analysis.ParametricRationalIntegralAnalyticity

Given a measure, a measurable integration set of finite measure, a polynomial degree, coefficient functions, and affine endpoint functions, an open parameter set, a positive separation margin, and coefficient bounds, openness and positivity, measurability of the coefficients and endpoints, a uniform coefficient bound, and uniform denominator separation throughout the parameter and integration sets, the polynomial-over-affine set integral is real analytic throughout the open parameter set.

Formal statement
hypotheses
α :
Type*
MeasurableSpace α
μ :
Measure α
K :
Set α
hK :
MeasurableSet K
hμK :
μ K ≠ ∞
N :
ℕ
c :
Fin (N + 1) → α → ℝ
a b :
α → ℝ
O :
Set ℝ
ε :
ℝ
C :
Fin (N + 1) → ℝ
hO :
IsOpen O
hε :
0 < ε
hc :
∀ i, Measurable (c i)
ha :
Measurable a
hb :
Measurable b
hc_bound :
∀ i, ∀ x ∈ K, |c i x| ≤ C i
hden :
∀ t ∈ O, ∀ x ∈ K, ε ≤ |affineDenominator a b t x|
conclusion
AnalyticOnNhd ℝ (fun t ↦ ∫ x in K, polynomialNumerator N c t x / affineDenominator a b t x ∂μ) O
Proof (Lean source)
theorem analyticOnNhd_setIntegral_polynomial_div_affine_of_uniform_nonzero {α : Type*} [MeasurableSpace α] (μ : Measure α) {K : Set α} (hK : MeasurableSet K) (hμK : μ K ≠ ∞) (N : ℕ) (c : Fin (N + 1) → α → ℝ) (a b : α → ℝ) (O : Set ℝ) (ε : ℝ) (C : Fin (N + 1) → ℝ) (hO : IsOpen O) (hε : 0 < ε) (hc : ∀ i, Measurable (c i)) (ha : Measurable a) (hb : Measurable b) (hc_bound : ∀ i, ∀ x ∈ K, |c i x| ≤ C i) (hden : ∀ t ∈ O, ∀ x ∈ K, ε ≤ |affineDenominator a b t x|) : AnalyticOnNhd ℝ (fun t ↦ ∫ x in K, polynomialNumerator N c t x / affineDenominator a b t x ∂μ) O := by -- Unfold `AnalyticOnNhd` pointwise. Openness supplies a positive parameter ball contained -- in `O`; restrict `hden` to that ball and apply the preceding ball-local theorem. intro t₀ ht₀ rcases affineDenominator_uniformly_nonzero_on_open_near hO hε hden ht₀ with ⟨r, hr, _hball, hden_ball⟩ exact analyticAt_setIntegral_polynomial_div_affine_of_uniform_nonzero_near μ hK hμK N c a b t₀ ε r C hε hr hc ha hb hc_bound fun t ht ↦ hden_ball t (by simpa [Metric.mem_ball, Real.dist_eq] using ht)
Causalean.Mathlib.Analysis.ParametricRationalIntegralAnalyticity.analyticOnNhd_setIntegral_polynomial_div_affine_of_uniform_nonzero · Causalean/Mathlib/Analysis/ParametricRationalIntegralAnalyticity/Main.lean:381 · uses affineDenominator , polynomialNumerator
4 supporting declarations (lemmas, instances)
  • analyticAt_setIntegral_polynomial_div_affine theorem — Given a measure, a measurable integration set of finite measure, a polynomial degree, coefficient functions, and affine endpoint functions, an expansion center, positive separation margin, nonnegative slope bound, and coefficient bounds, positivity and nonnegativity of those bounds, measurability of the coefficients and endpoints, uniform coefficient and slope bounds on the integration set, and uniform separation of the central denominator from zero, the polynomial-over-affine set integral is real analytic at the expansion center.
    hypotheses
    α :
    Type*
    MeasurableSpace α
    μ :
    Measure α
    K :
    Set α
    hK :
    MeasurableSet K
    hμK :
    μ K ≠ ∞
    N :
    ℕ
    c :
    Fin (N + 1) → α → ℝ
    a b :
    α → ℝ
    t₀ ε L :
    ℝ
    C :
    Fin (N + 1) → ℝ
    hε :
    0 < ε
    hL :
    0 ≤ L
    hc :
    ∀ i, Measurable (c i)
    ha :
    Measurable a
    hb :
    Measurable b
    hc_bound :
    ∀ i, ∀ x ∈ K, |c i x| ≤ C i
    hslope :
    ∀ x ∈ K, |b x - a x| ≤ L
    hden :
    ∀ x ∈ K, ε ≤ |affineDenominator a b t₀ x|
    conclusion
    AnalyticAt ℝ (fun t ↦ ∫ x in K, polynomialNumerator N c t x / affineDenominator a b t x ∂μ) t₀
    Proof (Lean source)
    theorem analyticAt_setIntegral_polynomial_div_affine {α : Type*} [MeasurableSpace α] (μ : Measure α) {K : Set α} (hK : MeasurableSet K) (hμK : μ K ≠ ∞) (N : ℕ) (c : Fin (N + 1) → α → ℝ) (a b : α → ℝ) (t₀ ε L : ℝ) (C : Fin (N + 1) → ℝ) (hε : 0 < ε) (hL : 0 ≤ L) (hc : ∀ i, Measurable (c i)) (ha : Measurable a) (hb : Measurable b) (hc_bound : ∀ i, ∀ x ∈ K, |c i x| ≤ C i) (hslope : ∀ x ∈ K, |b x - a x| ≤ L) (hden : ∀ x ∈ K, ε ≤ |affineDenominator a b t₀ x|) : AnalyticAt ℝ (fun t ↦ ∫ x in K, polynomialNumerator N c t x / affineDenominator a b t x ∂μ) t₀ := by -- Proof route: work with `μ.restrict K`, whose finiteness follows from `hμK`. For each -- numerator coefficient `i`, expand `c i x / affineDenominator a b t x` geometrically at -- `t₀` and apply `analyticAt_integral_of_powerSeries_domination`. A radius proportional to -- `ε / (L + 1)` makes the coefficient majorant geometric. Finally pull the scalar `t ^ i` -- through the integral and use the finite-sum/product analytic closure lemmas. letI : IsFiniteMeasure (μ.restrict K) := isFiniteMeasure_restrict.mpr hμK let r : ℝ := ε / (2 * (L + 1)) let coeff : Fin (N + 1) → ℕ → α → ℝ := fun i n x ↦ c i x * ((-(b x - a x) / affineDenominator a b t₀ x) ^ n / affineDenominator a b t₀ x) let M : Fin (N + 1) → ℕ → ℝ := fun i n ↦ |C i| * (((L + 1) / ε) ^ n / ε) have hL1 : 0 < L + 1 := by linarith have hr : 0 < r := by dsimp [r] positivity have hd_meas : Measurable (fun x ↦ affineDenominator a b t₀ x) := by unfold affineDenominator fun_prop have hcoeff_meas (i : Fin (N + 1)) (n : ℕ) : AEStronglyMeasurable (coeff i n) (μ.restrict K) := by apply Measurable.aestronglyMeasurable dsimp [coeff] fun_prop have hM_nonneg (i : Fin (N + 1)) (n : ℕ) : 0 ≤ M i n := by dsimp [M] positivity have hcoeff_bound (i : Fin (N + 1)) (n : ℕ) : ∀ᵐ x ∂μ.restrict K, ‖coeff i n x‖ ≤ M i n := by filter_upwards [ae_restrict_mem hK] with x hx have hci : |c i x| ≤ |C i| := (hc_bound i x hx).trans (le_abs_self _) have hd : ε ≤ |affineDenominator a b t₀ x| := hden x hx have hdpos : 0 < |affineDenominator a b t₀ x| := hε.trans_le hd have hs : |b x - a x| ≤ L + 1 := (hslope x hx).trans (by linarith) dsimp [coeff, M] rw [abs_mul, abs_div, abs_pow, abs_div, abs_neg] gcongr have hM_summable (i : Fin (N + 1)) : Summable (fun n ↦ M i n * r ^ n) := by have hbase : ((L + 1) / ε) * r = (1 : ℝ) / 2 := by dsimp [r] field_simp have heq : (fun n ↦ M i n * r ^ n) = (fun n ↦ (|C i| / ε) * ((1 : ℝ) / 2) ^ n) := by funext n dsimp [M] rw [← hbase] rw [mul_pow] ring rw [heq] exact summable_geometric_two.mul_left (|C i| / ε) have hseries (i : Fin (N + 1)) : ∀ t, |t - t₀| < r → ∀ᵐ x ∂μ.restrict K, c i x / affineDenominator a b t x = ∑' n : ℕ, coeff i n x * (t - t₀) ^ n := by intro t ht filter_upwards [ae_restrict_mem hK] with x hx have hd : ε ≤ |affineDenominator a b t₀ x| := hden x hx have hdpos : 0 < |affineDenominator a b t₀ x| := hε.trans_le hd have hs : |b x - a x| ≤ L + 1 := (hslope x hx).trans (by linarith) have hsmall : |(t - t₀) * (b x - a x) / affineDenominator a b t₀ x| < 1 := by calc |(t - t₀) * (b x - a x) / affineDenominator a b t₀ x| = |t - t₀| * |b x - a x| / |affineDenominator a b t₀ x| := by rw [abs_div, abs_mul] _ ≤ |t - t₀| * (L + 1) / |affineDenominator a b t₀ x| := by gcongr _ < r * (L + 1) / |affineDenominator a b t₀ x| := by gcongr _ ≤ r * (L + 1) / ε := by gcongr _ = 1 / 2 := by dsimp [r] field_simp _ < 1 := by norm_num have hrec := affineDenominator_reciprocal_eq_tsum (a := a) (b := b) (t := t) (t₀ := t₀) (x := x) (abs_pos.mp hdpos) hsmall calc c i x / affineDenominator a b t x = c i x * (affineDenominator a b t x)⁻¹ := div_eq_mul_inv _ _ _ = c i x * ∑' n : ℕ, ((-(b x - a x) / affineDenominator a b t₀ x) ^ n / affineDenominator a b t₀ x) * (t - t₀) ^ n := by rw [hrec] _ = ∑' n : ℕ, c i x * (((-(b x - a x) / affineDenominator a b t₀ x) ^ n / affineDenominator a b t₀ x) * (t - t₀) ^ n) := by rw [tsum_mul_left] _ = ∑' n : ℕ, coeff i n x * (t - t₀) ^ n := by apply tsum_congr intro n dsimp [coeff] ring have hAi (i : Fin (N + 1)) : AnalyticAt ℝ (fun t ↦ ∫ x, c i x / affineDenominator a b t x ∂μ.restrict K) t₀ := analyticAt_integral_of_powerSeries_domination (μ.restrict K) (fun t x ↦ c i x / affineDenominator a b t x) (coeff i) (M i) t₀ r hr (hcoeff_meas i) (hM_nonneg i) (hcoeff_bound i) (hM_summable i) (hseries i) have hsum : AnalyticAt ℝ (fun t ↦ ∑ i : Fin (N + 1), t ^ (i : ℕ) * ∫ x, c i x / affineDenominator a b t x ∂μ.restrict K) t₀ := by apply ((Finset.univ : Finset (Fin (N + 1))).analyticAt_sum (f := fun (i : Fin (N + 1)) (t : ℝ) ↦ t ^ (i : ℕ) * ∫ x, c i x / affineDenominator a b t x ∂μ.restrict K) (fun (i : Fin (N + 1)) _ ↦ (analyticAt_id.pow (i : ℕ)).mul (hAi i))).congr exact Filter.Eventually.of_forall (fun t ↦ by simp) apply hsum.congr rcases affineDenominator_uniformly_nonzero_near hε hL hden hslope with ⟨δ, hδ, hden_near⟩ filter_upwards [Metric.ball_mem_nhds t₀ hδ] with t ht have hd_t_meas : Measurable (fun x ↦ affineDenominator a b t x) := by unfold affineDenominator fun_prop have hfi (i : Fin (N + 1)) : Integrable (fun x ↦ t ^ (i : ℕ) * (c i x / affineDenominator a b t x)) (μ.restrict K) := by apply Integrable.const_mul apply Integrable.of_bound ((hc i).div hd_t_meas).aestronglyMeasurable (|C i| / (ε / 2)) filter_upwards [ae_restrict_mem hK] with x hx have hci : |c i x| ≤ |C i| := (hc_bound i x hx).trans (le_abs_self _) have hd : ε / 2 ≤ |affineDenominator a b t x| := hden_near t (by simpa [Real.dist_eq] using ht) x hx have hdpos : 0 < |affineDenominator a b t x| := (half_pos hε).trans_le hd change |c i x / affineDenominator a b t x| ≤ |C i| / (ε / 2) rw [abs_div] gcongr simp only [polynomialNumerator] have hpoint : (fun x ↦ (∑ i : Fin (N + 1), c i x * t ^ (i : ℕ)) / affineDenominator a b t x) = (fun x ↦ ∑ i : Fin (N + 1), t ^ (i : ℕ) * (c i x / affineDenominator a b t x)) := by funext x rw [Finset.sum_div] apply Finset.sum_congr rfl intro i hi ring rw [hpoint] rw [integral_finsetSum Finset.univ (fun i _ ↦ hfi i)] simp only [integral_const_mul]
    Causalean.Mathlib.Analysis.ParametricRationalIntegralAnalyticity.analyticAt_setIntegral_polynomial_div_affine · Causalean/Mathlib/Analysis/ParametricRationalIntegralAnalyticity/Main.lean:17
  • analyticOnNhd_setIntegral_polynomial_div_affine theorem — Given a measure, a measurable integration set of finite measure, a polynomial degree, coefficient functions, and affine endpoint functions, an open parameter set, positive separation margin, nonnegative slope bound, and coefficient bounds, openness and valid numerical bounds, measurability of the coefficients and endpoints, uniform coefficient and slope bounds on the integration set, and uniform denominator separation over the parameter and integration sets, the polynomial-over-affine set integral is real analytic throughout the open parameter set.
    hypotheses
    α :
    Type*
    MeasurableSpace α
    μ :
    Measure α
    K :
    Set α
    hK :
    MeasurableSet K
    hμK :
    μ K ≠ ∞
    N :
    ℕ
    c :
    Fin (N + 1) → α → ℝ
    a b :
    α → ℝ
    O :
    Set ℝ
    ε L :
    ℝ
    C :
    Fin (N + 1) → ℝ
    hO :
    IsOpen O
    hε :
    0 < ε
    hL :
    0 ≤ L
    hc :
    ∀ i, Measurable (c i)
    ha :
    Measurable a
    hb :
    Measurable b
    hc_bound :
    ∀ i, ∀ x ∈ K, |c i x| ≤ C i
    hslope :
    ∀ x ∈ K, |b x - a x| ≤ L
    hden :
    ∀ t ∈ O, ∀ x ∈ K, ε ≤ |affineDenominator a b t x|
    conclusion
    AnalyticOnNhd ℝ (fun t ↦ ∫ x in K, polynomialNumerator N c t x / affineDenominator a b t x ∂μ) O
    Proof (Lean source)
    theorem analyticOnNhd_setIntegral_polynomial_div_affine {α : Type*} [MeasurableSpace α] (μ : Measure α) {K : Set α} (hK : MeasurableSet K) (hμK : μ K ≠ ∞) (N : ℕ) (c : Fin (N + 1) → α → ℝ) (a b : α → ℝ) (O : Set ℝ) (ε L : ℝ) (C : Fin (N + 1) → ℝ) (hO : IsOpen O) (hε : 0 < ε) (hL : 0 ≤ L) (hc : ∀ i, Measurable (c i)) (ha : Measurable a) (hb : Measurable b) (hc_bound : ∀ i, ∀ x ∈ K, |c i x| ≤ C i) (hslope : ∀ x ∈ K, |b x - a x| ≤ L) (hden : ∀ t ∈ O, ∀ x ∈ K, ε ≤ |affineDenominator a b t x|) : AnalyticOnNhd ℝ (fun t ↦ ∫ x in K, polynomialNumerator N c t x / affineDenominator a b t x ∂μ) O := by -- `AnalyticOnNhd` is pointwise; specialize the preceding local theorem at each `t ∈ O`. intro t ht exact analyticAt_setIntegral_polynomial_div_affine μ hK hμK N c a b t ε L C hε hL hc ha hb hc_bound hslope (hden t ht)
    Causalean.Mathlib.Analysis.ParametricRationalIntegralAnalyticity.analyticOnNhd_setIntegral_polynomial_div_affine · Causalean/Mathlib/Analysis/ParametricRationalIntegralAnalyticity/Main.lean:172
  • analyticAt_setIntegral_polynomial_div_affine_of_slope_div_bound theorem — Given a measure, a measurable integration set of finite measure, a polynomial degree, coefficient functions, and affine endpoint functions, an expansion center, positive separation margin, nonnegative relative-slope bound, and coefficient bounds, positivity and nonnegativity of those bounds, measurability of the coefficients and endpoints, a uniform coefficient bound, a uniform relative affine-slope bound, and uniform central denominator separation, the polynomial-over-affine set integral is real analytic at the expansion center.
    hypotheses
    α :
    Type*
    MeasurableSpace α
    μ :
    Measure α
    K :
    Set α
    hK :
    MeasurableSet K
    hμK :
    μ K ≠ ∞
    N :
    ℕ
    c :
    Fin (N + 1) → α → ℝ
    a b :
    α → ℝ
    t₀ ε Q :
    ℝ
    C :
    Fin (N + 1) → ℝ
    hε :
    0 < ε
    hQ :
    0 ≤ Q
    hc :
    ∀ i, Measurable (c i)
    ha :
    Measurable a
    hb :
    Measurable b
    hc_bound :
    ∀ i, ∀ x ∈ K, |c i x| ≤ C i
    hratio :
    ∀ x ∈ K, |(b x - a x) / affineDenominator a b t₀ x| ≤ Q
    hden :
    ∀ x ∈ K, ε ≤ |affineDenominator a b t₀ x|
    conclusion
    AnalyticAt ℝ (fun t ↦ ∫ x in K, polynomialNumerator N c t x / affineDenominator a b t x ∂μ) t₀
    Proof (Lean source)
    theorem analyticAt_setIntegral_polynomial_div_affine_of_slope_div_bound {α : Type*} [MeasurableSpace α] (μ : Measure α) {K : Set α} (hK : MeasurableSet K) (hμK : μ K ≠ ∞) (N : ℕ) (c : Fin (N + 1) → α → ℝ) (a b : α → ℝ) (t₀ ε Q : ℝ) (C : Fin (N + 1) → ℝ) (hε : 0 < ε) (hQ : 0 ≤ Q) (hc : ∀ i, Measurable (c i)) (ha : Measurable a) (hb : Measurable b) (hc_bound : ∀ i, ∀ x ∈ K, |c i x| ≤ C i) (hratio : ∀ x ∈ K, |(b x - a x) / affineDenominator a b t₀ x| ≤ Q) (hden : ∀ x ∈ K, ε ≤ |affineDenominator a b t₀ x|) : AnalyticAt ℝ (fun t ↦ ∫ x in K, polynomialNumerator N c t x / affineDenominator a b t x ∂μ) t₀ := by -- Proof route: repeat the dominated geometric-series argument from -- `analyticAt_setIntegral_polynomial_div_affine`, but majorize the reciprocal-series -- coefficient directly by `Q ^ n / ε`. Taking radius `1 / (2 * (Q + 1))` makes the -- scalar majorant geometric. The final finite-sum/integrability rewrite uses -- `affineDenominator_uniformly_nonzero_near_of_slope_div_bound`. letI : IsFiniteMeasure (μ.restrict K) := isFiniteMeasure_restrict.mpr hμK let r : ℝ := 1 / (2 * (Q + 1)) let coeff : Fin (N + 1) → ℕ → α → ℝ := fun i n x ↦ c i x * ((-(b x - a x) / affineDenominator a b t₀ x) ^ n / affineDenominator a b t₀ x) let M : Fin (N + 1) → ℕ → ℝ := fun i n ↦ |C i| * (Q ^ n / ε) have hQ1 : 0 < Q + 1 := by linarith have hr : 0 < r := by dsimp [r] positivity have hd_meas : Measurable (fun x ↦ affineDenominator a b t₀ x) := by unfold affineDenominator fun_prop have hcoeff_meas (i : Fin (N + 1)) (n : ℕ) : AEStronglyMeasurable (coeff i n) (μ.restrict K) := by apply Measurable.aestronglyMeasurable dsimp [coeff] fun_prop have hM_nonneg (i : Fin (N + 1)) (n : ℕ) : 0 ≤ M i n := by dsimp [M] positivity have hcoeff_bound (i : Fin (N + 1)) (n : ℕ) : ∀ᵐ x ∂μ.restrict K, ‖coeff i n x‖ ≤ M i n := by filter_upwards [ae_restrict_mem hK] with x hx have hci : |c i x| ≤ |C i| := (hc_bound i x hx).trans (le_abs_self _) have hd : ε ≤ |affineDenominator a b t₀ x| := hden x hx have hdpos : 0 < |affineDenominator a b t₀ x| := hε.trans_le hd have hrat : |(b x - a x) / affineDenominator a b t₀ x| ≤ Q := hratio x hx have hrat' : |-(b x - a x) / affineDenominator a b t₀ x| ≤ Q := by simpa only [abs_div, abs_neg] using hrat dsimp [coeff, M] rw [abs_mul, abs_div, abs_pow] gcongr have hM_summable (i : Fin (N + 1)) : Summable (fun n ↦ M i n * r ^ n) := by have hQr_nonneg : 0 ≤ Q * r := mul_nonneg hQ hr.le have hQr_le : Q * r ≤ (1 : ℝ) / 2 := by calc Q * r = Q / (2 * (Q + 1)) := by simp [r, div_eq_mul_inv] _ ≤ (1 : ℝ) / 2 := by apply (div_le_iff₀ (by positivity : 0 < 2 * (Q + 1))).2 nlinarith have hQr_norm : ‖Q * r‖ < (1 : ℝ) := by rw [Real.norm_eq_abs, abs_of_nonneg hQr_nonneg] exact hQr_le.trans_lt (by norm_num) have heq : (fun n ↦ M i n * r ^ n) = (fun n ↦ (|C i| / ε) * (Q * r) ^ n) := by funext n dsimp [M] rw [mul_pow] ring rw [heq] exact (summable_geometric_of_norm_lt_one hQr_norm).mul_left (|C i| / ε) have hseries (i : Fin (N + 1)) : ∀ t, |t - t₀| < r → ∀ᵐ x ∂μ.restrict K, c i x / affineDenominator a b t x = ∑' n : ℕ, coeff i n x * (t - t₀) ^ n := by intro t ht filter_upwards [ae_restrict_mem hK] with x hx have hd : ε ≤ |affineDenominator a b t₀ x| := hden x hx have hdpos : 0 < |affineDenominator a b t₀ x| := hε.trans_le hd have hrat : |(b x - a x) / affineDenominator a b t₀ x| ≤ Q := hratio x hx have hsmall : |(t - t₀) * (b x - a x) / affineDenominator a b t₀ x| < 1 := by calc |(t - t₀) * (b x - a x) / affineDenominator a b t₀ x| = |t - t₀| * |(b x - a x) / affineDenominator a b t₀ x| := by rw [mul_div_assoc, abs_mul] _ ≤ |t - t₀| * Q := by gcongr _ ≤ |t - t₀| * (Q + 1) := by gcongr linarith _ < r * (Q + 1) := mul_lt_mul_of_pos_right ht hQ1 _ = 1 / 2 := by dsimp [r] field_simp _ < 1 := by norm_num have hrec := affineDenominator_reciprocal_eq_tsum (a := a) (b := b) (t := t) (t₀ := t₀) (x := x) (abs_pos.mp hdpos) hsmall calc c i x / affineDenominator a b t x = c i x * (affineDenominator a b t x)⁻¹ := div_eq_mul_inv _ _ _ = c i x * ∑' n : ℕ, ((-(b x - a x) / affineDenominator a b t₀ x) ^ n / affineDenominator a b t₀ x) * (t - t₀) ^ n := by rw [hrec] _ = ∑' n : ℕ, c i x * (((-(b x - a x) / affineDenominator a b t₀ x) ^ n / affineDenominator a b t₀ x) * (t - t₀) ^ n) := by rw [tsum_mul_left] _ = ∑' n : ℕ, coeff i n x * (t - t₀) ^ n := by apply tsum_congr intro n dsimp [coeff] ring have hAi (i : Fin (N + 1)) : AnalyticAt ℝ (fun t ↦ ∫ x, c i x / affineDenominator a b t x ∂μ.restrict K) t₀ := analyticAt_integral_of_powerSeries_domination (μ.restrict K) (fun t x ↦ c i x / affineDenominator a b t x) (coeff i) (M i) t₀ r hr (hcoeff_meas i) (hM_nonneg i) (hcoeff_bound i) (hM_summable i) (hseries i) have hsum : AnalyticAt ℝ (fun t ↦ ∑ i : Fin (N + 1), t ^ (i : ℕ) * ∫ x, c i x / affineDenominator a b t x ∂μ.restrict K) t₀ := by apply ((Finset.univ : Finset (Fin (N + 1))).analyticAt_sum (f := fun (i : Fin (N + 1)) (t : ℝ) ↦ t ^ (i : ℕ) * ∫ x, c i x / affineDenominator a b t x ∂μ.restrict K) (fun (i : Fin (N + 1)) _ ↦ (analyticAt_id.pow (i : ℕ)).mul (hAi i))).congr exact Filter.Eventually.of_forall (fun t ↦ by simp) apply hsum.congr rcases affineDenominator_uniformly_nonzero_near_of_slope_div_bound hε hQ hden hratio with ⟨δ, hδ, hden_near⟩ filter_upwards [Metric.ball_mem_nhds t₀ hδ] with t ht have hd_t_meas : Measurable (fun x ↦ affineDenominator a b t x) := by unfold affineDenominator fun_prop have hfi (i : Fin (N + 1)) : Integrable (fun x ↦ t ^ (i : ℕ) * (c i x / affineDenominator a b t x)) (μ.restrict K) := by apply Integrable.const_mul apply Integrable.of_bound ((hc i).div hd_t_meas).aestronglyMeasurable (|C i| / (ε / 2)) filter_upwards [ae_restrict_mem hK] with x hx have hci : |c i x| ≤ |C i| := (hc_bound i x hx).trans (le_abs_self _) have hd : ε / 2 ≤ |affineDenominator a b t x| := hden_near t (by simpa [Real.dist_eq] using ht) x hx have hdpos : 0 < |affineDenominator a b t x| := (half_pos hε).trans_le hd change |c i x / affineDenominator a b t x| ≤ |C i| / (ε / 2) rw [abs_div] gcongr simp only [polynomialNumerator] have hpoint : (fun x ↦ (∑ i : Fin (N + 1), c i x * t ^ (i : ℕ)) / affineDenominator a b t x) = (fun x ↦ ∑ i : Fin (N + 1), t ^ (i : ℕ) * (c i x / affineDenominator a b t x)) := by funext x rw [Finset.sum_div] apply Finset.sum_congr rfl intro i hi ring rw [hpoint] rw [integral_finsetSum Finset.univ (fun i _ ↦ hfi i)] simp only [integral_const_mul]
    Causalean.Mathlib.Analysis.ParametricRationalIntegralAnalyticity.analyticAt_setIntegral_polynomial_div_affine_of_slope_div_bound · Causalean/Mathlib/Analysis/ParametricRationalIntegralAnalyticity/Main.lean:190
  • analyticAt_setIntegral_polynomial_div_affine_of_uniform_nonzero_near theorem — Given a measure, a measurable integration set of finite measure, a polynomial degree, coefficient functions, and affine endpoint functions, a center, positive separation margin and radius, and coefficient bounds, positive numerical bounds, measurability of the coefficients and endpoints, a uniform coefficient bound, and uniform denominator separation throughout the parameter ball, the polynomial-over-affine set integral is real analytic at the ball center.
    hypotheses
    α :
    Type*
    MeasurableSpace α
    μ :
    Measure α
    K :
    Set α
    hK :
    MeasurableSet K
    hμK :
    μ K ≠ ∞
    N :
    ℕ
    c :
    Fin (N + 1) → α → ℝ
    a b :
    α → ℝ
    t₀ ε r :
    ℝ
    C :
    Fin (N + 1) → ℝ
    hε :
    0 < ε
    hr :
    0 < r
    hc :
    ∀ i, Measurable (c i)
    ha :
    Measurable a
    hb :
    Measurable b
    hc_bound :
    ∀ i, ∀ x ∈ K, |c i x| ≤ C i
    hden :
    ∀ t
    if
    |t - t₀| < r
    then
    ∀ x ∈ K, ε ≤ |affineDenominator a b t x|
    conclusion
    AnalyticAt ℝ (fun t ↦ ∫ x in K, polynomialNumerator N c t x / affineDenominator a b t x ∂μ) t₀
    Proof (Lean source)
    theorem analyticAt_setIntegral_polynomial_div_affine_of_uniform_nonzero_near {α : Type*} [MeasurableSpace α] (μ : Measure α) {K : Set α} (hK : MeasurableSet K) (hμK : μ K ≠ ∞) (N : ℕ) (c : Fin (N + 1) → α → ℝ) (a b : α → ℝ) (t₀ ε r : ℝ) (C : Fin (N + 1) → ℝ) (hε : 0 < ε) (hr : 0 < r) (hc : ∀ i, Measurable (c i)) (ha : Measurable a) (hb : Measurable b) (hc_bound : ∀ i, ∀ x ∈ K, |c i x| ≤ C i) (hden : ∀ t, |t - t₀| < r → ∀ x ∈ K, ε ≤ |affineDenominator a b t x|) : AnalyticAt ℝ (fun t ↦ ∫ x in K, polynomialNumerator N c t x / affineDenominator a b t x ∂μ) t₀ := by -- Derive the center-relative slope bound `r⁻¹` from the nonvanishing ball using -- `affineDenominator_slope_div_le_inv_radius`, then invoke the preceding theorem. have hden₀ : ∀ x ∈ K, ε ≤ |affineDenominator a b t₀ x| := hden t₀ (by simpa using hr) have hratio := affineDenominator_slope_div_le_inv_radius hr hε hden have hQ : 0 ≤ r⁻¹ := inv_nonneg.mpr (le_of_lt hr) exact analyticAt_setIntegral_polynomial_div_affine_of_slope_div_bound μ hK hμK N c a b t₀ ε r⁻¹ C hε hQ hc ha hb hc_bound hratio hden₀
    Causalean.Mathlib.Analysis.ParametricRationalIntegralAnalyticity.analyticAt_setIntegral_polynomial_div_affine_of_uniform_nonzero_near · Causalean/Mathlib/Analysis/ParametricRationalIntegralAnalyticity/Main.lean:359
Power­Series 1 core · 1 supporting This file packages the measure-theoretic core: a locally uniformly dominated scalar power series may be integrated coefficient by coefficient, and the resulting parameter function is analytic. ★ analyticAt_integral_of_powerSeries_domination

Dominated integration of scalar power series

This file packages the measure-theoretic core: a locally uniformly dominated scalar power series may be integrated coefficient by coefficient, and the resulting parameter function is analytic.

theorem analyticAt_integral_of_powerSeries_domination reviewed
Causalean.Mathlib.Analysis.ParametricRationalIntegralAnalyticity

Given a finite measure, an integrand family, its coefficient functions, coefficient envelopes, an expansion center and radius, a positive radius, measurable coefficients, nonnegative envelopes, almost-everywhere coefficient domination, a summable radius-weighted envelope, and an almost-everywhere pointwise power-series expansion throughout that radius, integrating the family produces a real-analytic function at the expansion center.

Formal statement
hypotheses
α :
Type*
MeasurableSpace α
μ :
Measure α
IsFiniteMeasure μ
f :
ℝ → α → ℝ
c :
ℕ → α → ℝ
M :
ℕ → ℝ
t₀ r :
ℝ
hr :
0 < r
hc :
∀ n, AEStronglyMeasurable (c n) μ
hM :
∀ n, 0 ≤ M n
hbound :
∀ n, ∀ᵐ x ∂μ, ‖c n x‖ ≤ M n
hsum :
Summable (fun n ↦ M n * r ^ n)
hseries :
∀ t
if
|t - t₀| < r
then
∀ᵐ x ∂μ, f t x = ∑' n : ℕ, c n x * (t - t₀) ^ n
conclusion
AnalyticAt ℝ (fun t ↦ ∫ x, f t x ∂μ) t₀
Proof (Lean source)
theorem analyticAt_integral_of_powerSeries_domination {α : Type*} [MeasurableSpace α] (μ : Measure α) [IsFiniteMeasure μ] (f : ℝ → α → ℝ) (c : ℕ → α → ℝ) (M : ℕ → ℝ) (t₀ r : ℝ) (hr : 0 < r) (hc : ∀ n, AEStronglyMeasurable (c n) μ) (hM : ∀ n, 0 ≤ M n) (hbound : ∀ n, ∀ᵐ x ∂μ, ‖c n x‖ ≤ M n) (hsum : Summable (fun n ↦ M n * r ^ n)) (hseries : ∀ t, |t - t₀| < r → ∀ᵐ x ∂μ, f t x = ∑' n : ℕ, c n x * (t - t₀) ^ n) : AnalyticAt ℝ (fun t ↦ ∫ x, f t x ∂μ) t₀ := by let a : ℕ → ℝ := fun n ↦ ∫ x, c n x ∂μ let p : FormalMultilinearSeries ℝ ℝ ℝ := FormalMultilinearSeries.ofScalars ℝ a let ρ : NNReal := ⟨r, hr.le⟩ have hc_int (n : ℕ) : Integrable (c n) μ := Integrable.of_bound (hc n) (M n) (hbound n) have ha_bound (n : ℕ) : ‖a n‖ ≤ μ.real univ * M n := by calc ‖a n‖ ≤ ∫ x, ‖c n x‖ ∂μ := norm_integral_le_integral_norm _ _ ≤ ∫ _x, M n ∂μ := by exact integral_mono_ae (hc_int n).norm (integrable_const _) (hbound n) _ = μ.real univ * M n := by simp have hp_bound (n : ℕ) : ‖p n‖ * (ρ : ℝ) ^ n ≤ μ.real univ * (M n * r ^ n) := by calc ‖p n‖ * (ρ : ℝ) ^ n = ‖a n‖ * r ^ n := by rw [show p = FormalMultilinearSeries.ofScalars ℝ a from rfl, FormalMultilinearSeries.ofScalars_norm] rfl _ ≤ (μ.real univ * M n) * r ^ n := mul_le_mul_of_nonneg_right (ha_bound n) (pow_nonneg hr.le n) _ = μ.real univ * (M n * r ^ n) := by ring have hp_sum : Summable (fun n ↦ ‖p n‖ * (ρ : ℝ) ^ n) := by apply Summable.of_nonneg_of_le · intro n exact mul_nonneg (norm_nonneg _) (pow_nonneg hr.le n) · exact hp_bound · exact hsum.mul_left (μ.real univ) have hρ_le : (ρ : ENNReal) ≤ p.radius := p.le_radius_of_summable_norm hp_sum have hp : HasFPowerSeriesOnBall (fun t ↦ ∫ x, f t x ∂μ) p t₀ ρ := by refine { r_le := hρ_le, r_pos := ?_, hasSum := ?_ } · exact ENNReal.coe_pos.mpr (show 0 < ρ from hr) · intro y hy have hyt : |(t₀ + y) - t₀| < r := by have hyrho : |y| < (ρ : ℝ) := by simpa [Metric.mem_eball, edist_dist, Real.dist_eq] using hy rw [show (ρ : ℝ) = r from rfl] at hyrho simpa using hyrho have hy_radius : y ∈ Metric.eball (0 : ℝ) p.radius := Metric.mem_eball.2 (lt_of_lt_of_le (Metric.mem_eball.1 hy) hρ_le) have hsum_y : Summable (fun n : ℕ ↦ p n fun _ ↦ y) := p.summable hy_radius rw [integral_eq_tsum_of_powerSeries_domination μ f c M t₀ r (t₀ + y) hr hyt hc hM hbound hsum hseries] simpa [p, a, FormalMultilinearSeries.ofScalars_apply_eq, mul_comm] using hsum_y.hasSum exact hp.analyticAt
Causalean.Mathlib.Analysis.ParametricRationalIntegralAnalyticity.analyticAt_integral_of_powerSeries_domination · Causalean/Mathlib/Analysis/ParametricRationalIntegralAnalyticity/PowerSeries.lean:57
1 supporting declaration (lemmas, instances)
  • integral_eq_tsum_of_powerSeries_domination theorem — Given a finite measure, an integrand family, its coefficient functions, coefficient envelopes, an expansion center, radius, and evaluation parameter, a positive radius and an evaluation inside it, measurable coefficients, nonnegative envelopes, almost-everywhere coefficient domination, a summable radius-weighted envelope, and an almost-everywhere pointwise power-series expansion, the integral equals the series of coefficient integrals at the evaluation parameter.
    hypotheses
    α :
    Type*
    MeasurableSpace α
    μ :
    Measure α
    IsFiniteMeasure μ
    f :
    ℝ → α → ℝ
    c :
    ℕ → α → ℝ
    M :
    ℕ → ℝ
    t₀ r t :
    ℝ
    hr :
    0 < r
    ht :
    |t - t₀| < r
    hc :
    ∀ n, AEStronglyMeasurable (c n) μ
    hM :
    ∀ n, 0 ≤ M n
    hbound :
    ∀ n, ∀ᵐ x ∂μ, ‖c n x‖ ≤ M n
    hsum :
    Summable (fun n ↦ M n * r ^ n)
    hseries :
    ∀ s
    if
    |s - t₀| < r
    then
    ∀ᵐ x ∂μ, f s x = ∑' n : ℕ, c n x * (s - t₀) ^ n
    conclusion
    ∫ x, f t x ∂μ = ∑' n : ℕ, (∫ x, c n x ∂μ) * (t - t₀) ^ n
    Proof (Lean source)
    theorem integral_eq_tsum_of_powerSeries_domination {α : Type*} [MeasurableSpace α] (μ : Measure α) [IsFiniteMeasure μ] (f : ℝ → α → ℝ) (c : ℕ → α → ℝ) (M : ℕ → ℝ) (t₀ r t : ℝ) (hr : 0 < r) (ht : |t - t₀| < r) (hc : ∀ n, AEStronglyMeasurable (c n) μ) (hM : ∀ n, 0 ≤ M n) (hbound : ∀ n, ∀ᵐ x ∂μ, ‖c n x‖ ≤ M n) (hsum : Summable (fun n ↦ M n * r ^ n)) (hseries : ∀ s, |s - t₀| < r → ∀ᵐ x ∂μ, f s x = ∑' n : ℕ, c n x * (s - t₀) ^ n) : ∫ x, f t x ∂μ = ∑' n : ℕ, (∫ x, c n x ∂μ) * (t - t₀) ^ n := by let F : ℕ → α → ℝ := fun n x ↦ c n x * (t - t₀) ^ n have hc_int (n : ℕ) : Integrable (c n) μ := Integrable.of_bound (hc n) (M n) (hbound n) have hF_int (n : ℕ) : Integrable (F n) μ := (hc_int n).mul_const _ have hF_bound (n : ℕ) : ∫ x, ‖F n x‖ ∂μ ≤ μ.real univ * (M n * r ^ n) := by calc ∫ x, ‖F n x‖ ∂μ ≤ ∫ _x, M n * r ^ n ∂μ := by apply integral_mono_ae (hF_int n).norm (integrable_const _) filter_upwards [hbound n] with x hx simp only [F, norm_mul, Real.norm_eq_abs, abs_pow] exact mul_le_mul hx (pow_le_pow_left₀ (abs_nonneg _) (le_of_lt ht) n) (pow_nonneg (abs_nonneg _) n) (hM n) _ = μ.real univ * (M n * r ^ n) := by simp have hF_sum : Summable (fun n ↦ ∫ x, ‖F n x‖ ∂μ) := by apply Summable.of_nonneg_of_le · exact fun n ↦ integral_nonneg (fun x ↦ norm_nonneg (F n x)) · exact hF_bound · exact hsum.mul_left (μ.real univ) calc ∫ x, f t x ∂μ = ∫ x, ∑' n, F n x ∂μ := integral_congr_ae (hseries t ht) _ = ∑' n, ∫ x, F n x ∂μ := (integral_tsum_of_summable_integral_norm hF_int hF_sum).symm _ = ∑' n, (∫ x, c n x ∂μ) * (t - t₀) ^ n := by apply tsum_congr intro n exact integral_mul_const _ _
    Causalean.Mathlib.Analysis.ParametricRationalIntegralAnalyticity.integral_eq_tsum_of_powerSeries_domination · Causalean/Mathlib/Analysis/ParametricRationalIntegralAnalyticity/PowerSeries.lean:16