OutsideChangeOfMeasure.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Outside-coordinate change of measure for the actual resampling transition

The observable may depend on the same Bernoulli set used at every other tree node. The only locality required here is that it ignores the fixed target's incoming label. No independence between different tree nodes is assumed.

def OAI.LeanBlast.SecondKahnKalai.cutoffTargetMass line 28
Source documentation
Actual target marginal restricted to the event that the density is at least δ.
```
def cutoffTargetMass (ν : FiniteLaw B) (A : B → Finset X) (p δ : ℝ)
    (W : Finset X) (b : B) : ℝ :=
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw
theorem OAI.LeanBlast.SecondKahnKalai.cutoffTargetMass_nonneg line 33

theorem OAI.LeanBlast.SecondKahnKalai.cutoffTargetMass_mul_eq_expectation line 44

Source documentation

This marginal is the literal conditional expectation of the target-and-density event.

theorem cutoffTargetMass_mul_eq_expectation (ν : FiniteLaw B) (A : B → Finset X)
    {p : ℝ} (hν : ν.IsPositive) (hp : 0 < p) (δ : ℝ)
    (W : Finset X) (b : B) (f : Finset X → ℝ) :
    cutoffTargetMass ν A p δ W b * f W =
      (resamplingLaw ν A p W hν hp).expectation
        (fun cb => if cb.2 = b ∧ δ ≤ resamplingZ ν A p (resamplingY A W cb.1)
          then f W else 0) := by
…

Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.cutoffTargetMass, OAI.LeanBlast.SecondKahnKalai.resamplingLaw, OAI.LeanBlast.SecondKahnKalai.resamplingZ, OAI.LeanBlast.SecondKahnKalai.resamplingY

theorem OAI.LeanBlast.SecondKahnKalai.subset_union_iff_sdiff_subset line 60
theorem OAI.LeanBlast.SecondKahnKalai.dependsOutside_union line 72
Source documentation
Modifying only coordinates inside the ignored label leaves the observable unchanged.
```
theorem dependsOutside_union {β : Type*} (A S : Finset X) (f : Finset X → β)
    (hf : DependsOutside A f) (hSA : S ⊆ A) (W : Finset X) :
    f (W ∪ S) = f W := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.DependsOutside
theorem OAI.LeanBlast.SecondKahnKalai.inv_pow_card_mul_pow_sdiff line 85
theorem OAI.LeanBlast.SecondKahnKalai.cutoff_source_weight_le line 97
Source documentation
The only pointwise change of density is the reciprocal cutoff. The remaining event uses coordinates inside the fixed target label.
```
theorem cutoff_source_weight_le (ν : FiniteLaw B) (A : B → Finset X)
    {p δ : ℝ} (hp : 0 ≤ p) (hδ : 0 < δ) (W : Finset X) (c b : B) :
    (if δ ≤ resamplingZ ν A p (resamplingY A W c)
      then resamplingWeight ν A p W (c, b) else 0) ≤
      if A b \ A c ⊆ W then δ⁻¹ * ν.weight c * ν.weight b * (p⁻¹) ^ (A b).card
      else 0 := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.resamplingZ, OAI.LeanBlast.SecondKahnKalai.resamplingY, OAI.LeanBlast.SecondKahnKalai.resamplingWeight
theorem OAI.LeanBlast.SecondKahnKalai.bernoulli_subset_expectation_of_dependsOutside line 129
Source documentation
A containment event on ignored coordinates is independent of the observable. This is derived from the fixed-union formula for the actual Bernoulli product weights.
```
theorem bernoulli_subset_expectation_of_dependsOutside
    {p : ℝ} (hp : p ≠ 0) (A S : Finset X) (f : Finset X → ℝ)
    (hf : DependsOutside A f) (hSA : S ⊆ A) :
    bernoulliExpectation p (fun W => if S ⊆ W then f W else 0) =
      p ^ S.card * bernoulliExpectation p f := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.DependsOutside, OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation

theorem OAI.LeanBlast.SecondKahnKalai.outside_change_of_measure_moment line 152

Source documentation

Change of measure before applying spread: the exact loss is the intersection moment.

theorem outside_change_of_measure_moment (ν : FiniteLaw B) (A : B → Finset X)
    {p δ : ℝ} (hp : 0 < p) (hp1 : p ≤ 1) (hδ : 0 < δ)
    (b : B) (f : Finset X → ℝ) (hf : ∀ W, 0 ≤ f W)
    (hloc : DependsOutside (A b) f) :
    bernoulliExpectation p (fun W => cutoffTargetMass ν A p δ W b * f W) ≤
      δ⁻¹ * ν.weight b * bernoulliExpectation p f *
        ν.expectation (fun c => (p⁻¹) ^ (A c ∩ A b).card) := by
…

Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.DependsOutside, OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation, OAI.LeanBlast.SecondKahnKalai.cutoffTargetMass

theorem OAI.LeanBlast.SecondKahnKalai.outside_change_of_measure line 212

theorem OAI.LeanBlast.SecondKahnKalai.outside_change_of_measure_of_le line 247

Source documentation

Any smaller target mass, including local non-failure, obeys the same bound.

theorem outside_change_of_measure_of_le (ν : FiniteLaw B) (A : B → Finset X)
    {p a : ℝ} (hp : 0 < p) (hp1 : p ≤ 1) (ha : 0 ≤ a)
    (hs : IsSpread ν A a) (m : ℕ) (b : B) (hAb : (A b).card ≤ m)
    (hsmall : a / p ≤ Real.exp (-50))
    (f : Finset X → ℝ) (hf : ∀ W, 0 ≤ f W) (hloc : DependsOutside (A b) f)
    (t : Finset X → ℝ)
    (ht : ∀ W, t W ≤ cutoffTargetMass ν A p (Real.exp (-10 * (m : ℝ))) W b) :
    bernoulliExpectation p (fun W => t W * f W) ≤
      Real.exp (11 * (m : ℝ)) * ν.weight b * bernoulliExpectation p f := by
…

Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.IsSpread, OAI.LeanBlast.SecondKahnKalai.DependsOutside, OAI.LeanBlast.SecondKahnKalai.cutoffTargetMass, OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation

theorem OAI.LeanBlast.SecondKahnKalai.outside_change_of_measure_law line 264

Source documentation

The same inequality stated as the expectation of the actual transition event.

theorem outside_change_of_measure_law (ν : FiniteLaw B) (A : B → Finset X)
    (hν : ν.IsPositive) {p a : ℝ} (hp : 0 < p) (hp1 : p ≤ 1) (ha : 0 ≤ a)
    (hs : IsSpread ν A a) (m : ℕ) (b : B) (hAb : (A b).card ≤ m)
    (hsmall : a / p ≤ Real.exp (-50))
    (f : Finset X → ℝ) (hf : ∀ W, 0 ≤ f W) (hloc : DependsOutside (A b) f) :
    bernoulliExpectation p (fun W =>
      (resamplingLaw ν A p W hν hp).expectation
        (fun cb => if cb.2 = b ∧ Real.exp (-10 * (m : ℝ)) ≤
            resamplingZ ν A p (resamplingY A W cb.1) then f W else 0)) ≤
      Real.exp (11 * (m : ℝ)) * ν.weight b * bernoulliExpectation p f := by
…

Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.IsSpread, OAI.LeanBlast.SecondKahnKalai.DependsOutside, OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation, OAI.LeanBlast.SecondKahnKalai.resamplingLaw, OAI.LeanBlast.SecondKahnKalai.resamplingZ, OAI.LeanBlast.SecondKahnKalai.resamplingY