def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9WeightedSource : Set (ℝ × ℝ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9WeightedSource = {x : ℝ × ℝ | x.1 ∈ Set.Ioc (4 / 53) (1 / 10) ∧ x.2 ∈ Set.Ioc (1 / 3) ((1 - x.1) / 2)}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9WeightedIntegrand (x : ℝ × ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9WeightedIntegrand x = 1 / (x.1 * x.2 * (1 - x.1 - x.2) * (1 - x.1))

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9WeightedUpperIntegrand (n : ℕ) (h : ℝ) (x : ℝ × ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9WeightedUpperIntegrand n h x = ∑ q ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegralCells n h, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegralCorner n 0 q * (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridCell n q).indicator MathlibNt.SieveTheory.LiuWeight.liuLogDensity x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_fouvryG9WeightedSource : MeasurableSet fouvryG9WeightedSource

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9WeightedSource_subset_ambient : fouvryG9WeightedSource ⊆ goldbachB9LogAmbientBox

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.continuousOn_fouvryG9WeightedIntegrand : ContinuousOn fouvryG9WeightedIntegrand goldbachB9LogAmbientBox

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.integrableOn_fouvryG9WeightedIntegrand {s : Set (ℝ × ℝ)} (hs : MeasurableSet s) (hsub : s ⊆ goldbachB9LogAmbientBox) : MeasureTheory.IntegrableOn fouvryG9WeightedIntegrand s MeasureTheory.volume

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.integrable_fouvryG9WeightedSourceIndicator : MeasureTheory.Integrable (fouvryG9WeightedSource.indicator fouvryG9WeightedIntegrand) MeasureTheory.volume

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegralLow_eq_iteratedSetIntegral : fouvryG9RelaxedIntegralLow = ∫ (u : ℝ) in Set.Ioc (4 / 53) (1 / 10), ∫ (v : ℝ) in Set.Ioc (1 / 3) ((1 - u) / 2), fouvryG9WeightedIntegrand (u, v)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9WeightedSourceIndicator_integral_section (u : ℝ) : ∫ (v : ℝ), fouvryG9WeightedSource.indicator fouvryG9WeightedIntegrand (u, v) = (Set.Ioc (4 / 53) (1 / 10)).indicator (fun (u : ℝ) => ∫ (v : ℝ) in Set.Ioc (1 / 3) ((1 - u) / 2), fouvryG9WeightedIntegrand (u, v)) u

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegralLow_eq_setIntegral : fouvryG9RelaxedIntegralLow = ∫ (x : ℝ × ℝ) in fouvryG9WeightedSource, fouvryG9WeightedIntegrand x

Fubini is applied to an integrable indicator, not to an unspecified integral.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.integrable_fouvryG9WeightedUpperIntegrand (n : ℕ) (hn : 0 < n) (h : ℝ) : MeasureTheory.Integrable (fouvryG9WeightedUpperIntegrand n h) MeasureTheory.volume

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegralUpperSum_eq_integral (n : ℕ) (hn : 0 < n) (h : ℝ) : fouvryG9RelaxedIntegralUpperSum n h 0 = ∫ (x : ℝ × ℝ), fouvryG9WeightedUpperIntegrand n h x

The selected-cell sum retains its actual logarithmic rectangle masses.