BandIncidence.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Weighted dust incidence

This is the dust part of eq:weighted-level-bound in Section 1 of 047-02. A point contributes its weight on a measurable set of levels. Tonelli converts the expected total incidence to the sum of weights times level probabilities; the band-incidence estimate bounds these probabilities, and square summability makes the result finite.

def OAI.CircleDomainRigidity.weightedBandIncidence line 25
theorem OAI.CircleDomainRigidity.measurable_weightedBandIncidence line 29
theorem OAI.CircleDomainRigidity.weightedBandIncidence_toReal_eq line 34

theorem OAI.CircleDomainRigidity.lintegral_weightedBandIncidence line 50

Source documentation

Tonelli's exact incidence identity.

theorem lintegral_weightedBandIncidence {T ι : Type*} [MeasurableSpace T] [Countable ι]
    (ν : Measure T) (E : ι → Set T) (m : ι → ℝ) (hE : ∀ s, MeasurableSet (E s)) :
    ∫⁻ t, weightedBandIncidence E m t ∂ν = ∑' s, ENNReal.ofReal (m s) * ν (E s) := by
…

Mentions: OAI.CircleDomainRigidity.weightedBandIncidence

theorem OAI.CircleDomainRigidity.lintegral_weightedBandIncidence_le line 62

Source documentation

The band probability bound yields the weighted-level dust estimate.

theorem lintegral_weightedBandIncidence_le {T ι : Type*} [MeasurableSpace T] [Countable ι]
    (ν : Measure T) (E : ι → Set T) (m a : ι → ℝ)
    (hE : ∀ s, MeasurableSet (E s)) (hm : ∀ s, 0 ≤ m s) (ha : ∀ s, 0 ≤ a s)
    (hband : ∀ s, ν (E s) ≤ ENNReal.ofReal (a s))
    (hm2 : Summable (fun s => m s ^ 2)) (ha2 : Summable (fun s => a s ^ 2)) :
    ∫⁻ t, weightedBandIncidence E m t ∂ν ≤ ENNReal.ofReal (∑' s, m s * a s) := by
…

Mentions: OAI.CircleDomainRigidity.weightedBandIncidence

theorem OAI.CircleDomainRigidity.tsum_mul_le_sqrt_square_sums line 78

Source documentation

The Cauchy--Schwarz bound for the weighted band series.

theorem tsum_mul_le_sqrt_square_sums {ι : Type*} (m a : ι → ℝ)
    (hm2 : Summable (fun s => m s ^ 2)) (ha2 : Summable (fun s => a s ^ 2)) :
    (∑' s, m s * a s) ≤ Real.sqrt (∑' s, m s ^ 2) * Real.sqrt (∑' s, a s ^ 2) := by
…

theorem OAI.CircleDomainRigidity.lintegral_weightedBandIncidence_lt_top line 89

theorem OAI.CircleDomainRigidity.ae_summable_weighted_band_series line 100

Source documentation

The weighted series is summable at almost every level.

theorem ae_summable_weighted_band_series
    {T ι : Type*} [MeasurableSpace T] [Countable ι]
    (ν : Measure T) (E : ι → Set T) (m a : ι → ℝ)
    (hE : ∀ s, MeasurableSet (E s)) (hm : ∀ s, 0 ≤ m s) (ha : ∀ s, 0 ≤ a s)
    (hband : ∀ s, ν (E s) ≤ ENNReal.ofReal (a s))
    (hm2 : Summable (fun s => m s ^ 2)) (ha2 : Summable (fun s => a s ^ 2)) :
    ∀ᵐ t ∂ν, Summable (fun s => (E s).indicator (fun _ => m s) t) := by
…

theorem OAI.CircleDomainRigidity.lintegral_weightedBandIncidence_le_cauchySchwarz line 116

theorem OAI.CircleDomainRigidity.integral_weightedBandIncidence_toReal_le line 129

Source documentation

The same bound as an ordinary real integral; the integrand is finite almost everywhere by its finite Tonelli integral.

theorem integral_weightedBandIncidence_toReal_le
    {T ι : Type*} [MeasurableSpace T] [Countable ι]
    (ν : Measure T) (E : ι → Set T) (m a : ι → ℝ)
    (hE : ∀ s, MeasurableSet (E s)) (hm : ∀ s, 0 ≤ m s) (ha : ∀ s, 0 ≤ a s)
    (hband : ∀ s, ν (E s) ≤ ENNReal.ofReal (a s))
    (hm2 : Summable (fun s => m s ^ 2)) (ha2 : Summable (fun s => a s ^ 2)) :
    Integrable (fun t => (weightedBandIncidence E m t).toReal) ν ∧
      (∫ t, (weightedBandIncidence E m t).toReal ∂ν) ≤ ∑' s, m s * a s := by
…

Mentions: OAI.CircleDomainRigidity.weightedBandIncidence

theorem OAI.CircleDomainRigidity.integral_weighted_band_series_le line 148

Source documentation

The paper's ordinary real weighted series is integrable and obeys the same dust contribution bound.

theorem integral_weighted_band_series_le
    {T ι : Type*} [MeasurableSpace T] [Countable ι]
    (ν : Measure T) (E : ι → Set T) (m a : ι → ℝ)
    (hE : ∀ s, MeasurableSet (E s)) (hm : ∀ s, 0 ≤ m s) (ha : ∀ s, 0 ≤ a s)
    (hband : ∀ s, ν (E s) ≤ ENNReal.ofReal (a s))
    (hm2 : Summable (fun s => m s ^ 2)) (ha2 : Summable (fun s => a s ^ 2)) :
    Integrable (fun t => ∑' s, (E s).indicator (fun _ => m s) t) ν ∧
      (∫ t, ∑' s, (E s).indicator (fun _ => m s) t ∂ν) ≤ ∑' s, m s * a s := by
…