Expected Query Slack expected resource le

lemma expectedQuerySlack_expected_resource_le    (impl : QueryImpl spec (StateT (σ × Bool) (OracleComp spec')))    (chargedQuery growthQuery : spec.Domain → Prop)    [DecidablePred chargedQuery] [DecidablePred growthQuery]    (R : σ → ℝ≥0∞) (ζ β g : ℝ≥0∞)    (h_charged : ∀ (t : spec.Domain) (p : σ × Bool), p.2 = false → chargedQuery t →      ∑' z : spec.Range t × σ × Bool, Pr[= z | (impl t).run p] * R z.2.1 ≤ R p.1 + g)    (h_growth : ∀ (t : spec.Domain) (p : σ × Bool), p.2 = false →      ¬ chargedQuery t → growthQuery t →      ∀ z ∈ support ((impl t).run p), R z.2.1 ≤ R p.1 + 1)    (h_free : ∀ (t : spec.Domain) (p : σ × Bool), p.2 = false →      ¬ chargedQuery t → ¬ growthQuery t →      ∀ z ∈ support ((impl t).run p), R z.2.1 ≤ R p.1)    (oa : OracleComp spec α) {qS qH : ℕ}    (h_qS : OracleComp.IsQueryBoundP oa chargedQuery qS)    (h_qH : OracleComp.IsQueryBoundP oa growthQuery qH)    (s : σ) :    expectedQuerySlack impl chargedQuery (fun s => ζ + R s * β) oa qS (s, false)      ≤ (qS : ℝ≥0∞) * ζ +        ((qS : ℝ≥0∞) * R s + (qS : ℝ≥0∞) * (qH : ℝ≥0∞) +          (qS.choose 2 : ℝ≥0∞) * g) * β := by  induction oa using OracleComp.inductionOn generalizing qS qH s with  | pure x => simp only [expectedQuerySlack_pure, zero_le]  | query_bind t cont ih =>      rw [isQueryBoundP_query_bind_iff] at h_qS h_qH      obtain ⟨hcanS, hcontS⟩ := h_qS      obtain ⟨hcanH, hcontH⟩ := h_qH      by_cases hSt : chargedQuery t      · simp only [hSt, if_true] at hcontS        have hqS_pos : 0 < qS := hcanS.resolve_left (· hSt)        obtain ⟨m, rfl⟩ : ∃ m, qS = m + 1 := ⟨qS - 1, by omega⟩        rw [expectedQuerySlack_query_bind,          expectedQuerySlackStep_costly_pos _ _ _ _ _ _ _ hSt hqS_pos]        simp only [Nat.add_sub_cancel] at hcontS ⊢        have h_sum_le : ∀ z : spec.Range t × σ × Bool,            Pr[= z | (impl t).run (s, false)] *              expectedQuerySlack impl chargedQuery (fun s => ζ + R s * β) (cont z.1) m z.2            ≤ Pr[= z | (impl t).run (s, false)] *                ((m : ℝ≥0∞) * ζ +                  ((m : ℝ≥0∞) * (qH : ℝ≥0∞) + (m.choose 2 : ℝ≥0∞) * g) * β)              + (m : ℝ≥0∞) * β * (Pr[= z | (impl t).run (s, false)] * R z.2.1) := by          rintro ⟨u, s', bad'⟩          cases bad' with          | true => simp          | false =>              have hIH : expectedQuerySlack impl chargedQuery (fun s => ζ + R s * β)                  (cont u) m (s', false)                  ≤ (m : ℝ≥0∞) * ζ + ((m : ℝ≥0∞) * R s' + (m : ℝ≥0∞) * (qH : ℝ≥0∞)                      + (m.choose 2 : ℝ≥0∞) * g) * β := by                have hqH'_le : (if growthQuery t then qH - 1 else qH) ≤ qH := by                  split_ifs <;> omega                refine (ih u (hcontS u) (hcontH u) s').trans ?_                gcongr              refine (mul_le_mul_right hIH _).trans (le_of_eq ?_)              ring        have h_tsum : (∑' z : spec.Range t × σ × Bool,              Pr[= z | (impl t).run (s, false)] *                expectedQuerySlack impl chargedQuery (fun s => ζ + R s * β) (cont z.1) m z.2)            ≤ ((m : ℝ≥0∞) * ζ +                ((m : ℝ≥0∞) * (qH : ℝ≥0∞) + (m.choose 2 : ℝ≥0∞) * g) * β)              + (m : ℝ≥0∞) * β * (R s + g) := by          refine (ENNReal.tsum_le_tsum h_sum_le).trans ?_          rw [ENNReal.tsum_add, ENNReal.tsum_mul_right, ENNReal.tsum_mul_left]          exact add_le_add            (mul_le_of_le_one_left (by positivity) tsum_probOutput_le_one)            (mul_le_mul_right (h_charged t (s, false) rfl hSt) _)        have hch : (((m + 1).choose 2 : ℕ) : ℝ≥0∞) = (m : ℝ≥0∞) + (m.choose 2 : ℝ≥0∞) := by          have hch_nat : (m + 1).choose 2 = m + m.choose 2 := by            rw [Nat.choose_succ_succ', Nat.choose_one_right]          exact_mod_cast hch_nat        calc ζ + R s * β + (∑' z : spec.Range t × σ × Bool,              Pr[= z | (impl t).run (s, false)] *                expectedQuerySlack impl chargedQuery (fun s => ζ + R s * β) (cont z.1) m z.2)            ≤ ζ + R s * β              + (((m : ℝ≥0∞) * ζ +                  ((m : ℝ≥0∞) * (qH : ℝ≥0∞) + (m.choose 2 : ℝ≥0∞) * g) * β)                + (m : ℝ≥0∞) * β * (R s + g)) := by gcongr          _ = ((m : ℝ≥0∞) + 1) * ζ              + (((m : ℝ≥0∞) + 1) * R s + (m : ℝ≥0∞) * (qH : ℝ≥0∞)                + ((m : ℝ≥0∞) + (m.choose 2 : ℝ≥0∞)) * g) * β := by ring          _ ≤ ((m : ℝ≥0∞) + 1) * ζ              + (((m : ℝ≥0∞) + 1) * R s + ((m : ℝ≥0∞) + 1) * (qH : ℝ≥0∞)                + ((m : ℝ≥0∞) + (m.choose 2 : ℝ≥0∞)) * g) * β := by              gcongr              exact le_self_add          _ = ((m + 1 : ℕ) : ℝ≥0∞) * ζ              + (((m + 1 : ℕ) : ℝ≥0∞) * R s + ((m + 1 : ℕ) : ℝ≥0∞) * (qH : ℝ≥0∞)                + (((m + 1).choose 2 : ℕ) : ℝ≥0∞) * g) * β := by              rw [Nat.cast_add_one, hch]      · simp only [hSt, if_false] at hcontS        rw [expectedQuerySlack_query_bind, expectedQuerySlackStep_free _ _ _ _ _ _ _ hSt]        have h_z : ∀ z ∈ support ((impl t).run (s, false)),            expectedQuerySlack impl chargedQuery (fun s => ζ + R s * β) (cont z.1) qS z.2              ≤ (qS : ℝ≥0∞) * ζ + ((qS : ℝ≥0∞) * R s + (qS : ℝ≥0∞) * (qH : ℝ≥0∞)                  + (qS.choose 2 : ℝ≥0∞) * g) * β := by          rintro ⟨u, s', bad'⟩ hz          cases bad' with          | true => simp          | false =>              refine (ih u (hcontS u) (hcontH u) s').trans ?_              by_cases hHt : growthQuery t              · have hqH_pos : 0 < qH := hcanH.resolve_left (· hHt)                have hqH_cast : ((qH - 1 : ℕ) : ℝ≥0∞) + 1 = (qH : ℝ≥0∞) := by                  exact_mod_cast Nat.sub_add_cancel hqH_pos                have hRs' : R s' ≤ R s + 1 := h_growth t (s, false) rfl hSt hHt _ hz                rw [if_pos hHt]                calc (qS : ℝ≥0∞) * ζ + ((qS : ℝ≥0∞) * R s'                        + (qS : ℝ≥0∞) * ((qH - 1 : ℕ) : ℝ≥0∞)                        + (qS.choose 2 : ℝ≥0∞) * g) * β                    ≤ (qS : ℝ≥0∞) * ζ + ((qS : ℝ≥0∞) * (R s + 1)                        + (qS : ℝ≥0∞) * ((qH - 1 : ℕ) : ℝ≥0∞)                        + (qS.choose 2 : ℝ≥0∞) * g) * β := by gcongr                  _ = (qS : ℝ≥0∞) * ζ + ((qS : ℝ≥0∞) * R s                        + (qS : ℝ≥0∞) * (((qH - 1 : ℕ) : ℝ≥0∞) + 1)                        + (qS.choose 2 : ℝ≥0∞) * g) * β := by ring                  _ = (qS : ℝ≥0∞) * ζ + ((qS : ℝ≥0∞) * R s + (qS : ℝ≥0∞) * (qH : ℝ≥0∞)                        + (qS.choose 2 : ℝ≥0∞) * g) * β := by rw [hqH_cast]              · have hRs' : R s' ≤ R s := h_free t (s, false) rfl hSt hHt _ hz                rw [if_neg hHt]                gcongr        calc (∑' z : spec.Range t × σ × Bool,              Pr[= z | (impl t).run (s, false)] *                expectedQuerySlack impl chargedQuery (fun s => ζ + R s * β) (cont z.1) qS z.2)            ≤ ∑' z : spec.Range t × σ × Bool,                Pr[= z | (impl t).run (s, false)] *                  ((qS : ℝ≥0∞) * ζ + ((qS : ℝ≥0∞) * R s + (qS : ℝ≥0∞) * (qH : ℝ≥0∞)                    + (qS.choose 2 : ℝ≥0∞) * g) * β) :=              ENNReal.tsum_le_tsum fun z => by                by_cases hz : z ∈ support ((impl t).run (s, false))                · exact mul_le_mul_right (h_z z hz) _                · simp [probOutput_eq_zero_of_not_mem_support hz]          _ ≤ (qS : ℝ≥0∞) * ζ + ((qS : ℝ≥0∞) * R s + (qS : ℝ≥0∞) * (qH : ℝ≥0∞)                + (qS.choose 2 : ℝ≥0∞) * g) * β := by              rw [ENNReal.tsum_mul_right]              exact mul_le_of_le_one_left (by positivity) tsum_probOutput_le_one